574 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key
604 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.19ms
868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
883 WARN Test worker d.u.i.k.s.ProofSettings No proof-settings could be loaded, using defaults java.io.FileNotFoundException: /home/runner/.key/proof-settings.props (No such file or directory)
at java.base/java.io.FileInputStream.open0(Native Method)
1816 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1823 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1825 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1825 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
3517 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
9618 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 8.75s
9693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key
9731 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.3ns
9747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof
9747 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.51ns
9752 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
13081 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s
13085 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut
14168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut
14200 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.15ms
14212 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof
14213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.71ns
14215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
17325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s
17326 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight
18424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight
18444 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.46ms
18449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof
18449 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.2ns
18452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
21677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s
21678 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1
22736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1
22742 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms
22745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof
22746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.24ms
22748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
25774 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
25775 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2
26756 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2
26761 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms
26764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof
26764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.91ns
26767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
29652 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s
29653 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos
30614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos
30656 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.6ms
30660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof
30661 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 419.01ns
30662 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
33547 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
33547 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg
34490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg
34519 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.16ms
34525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof
34525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.81ns
34527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
37376 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
37377 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt
38351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt
38355 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 688.32ns
38357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof
38358 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.71ns
38359 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
41215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
41215 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong
42164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong
42167 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 676.22ns
42170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof
42170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.11ns
42171 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
45038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
45039 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort
46010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort
46013 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.02ns
46016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof
46016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.31ns
46017 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
48889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
48890 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte
49855 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte
49858 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.12ns
49863 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof
49863 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.4ns
49865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
52824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
52825 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar
53797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar
53800 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.32ns
53803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof
53803 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 434.81ns
53804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
56613 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
56613 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1
57574 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1
57648 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.27ms
57650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof
57650 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.8ns
57651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
60572 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s
60572 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2
61566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2
61594 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.09ms
61598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof
61598 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.11ns
61599 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
64472 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
64473 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists
65403 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists
65575 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 161.81ms
65580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof
65581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.01ns
65582 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
68384 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
68384 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one
69352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one
69357 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms
69360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof
69360 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.1ns
69362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
72370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s
72371 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one
73302 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one
73305 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms
73307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof
73307 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.31ns
73308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
76165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
76166 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero
77123 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero
77164 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.75ms
77167 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof
77168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.01ms
77169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
80074 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
80075 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1
81051 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1
81073 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.1ms
81076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof
81076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.2ns
81078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
83985 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
83985 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2
84946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2
84991 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.52ms
84993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof
84993 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.3ns
84994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
88011 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
88011 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1
88966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1
88980 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.23ms
88982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof
88982 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.91ns
88984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
92100 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s
92100 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2
93042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2
93054 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.31ms
93056 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof
93056 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns
93057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
95969 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
95970 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1
96893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1
96911 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.53ms
96913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof
96913 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.9ns
96914 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
99781 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
99781 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2
100684 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2
100695 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.94ms
100697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof
100697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns
100698 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
103505 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
103506 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom
104406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom
104440 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.76ms
104442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof
104443 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.11ns
104444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
107246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
107246 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus
108146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus
108194 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.17ms
108196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof
108196 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.6ns
108197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
111025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
111026 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom
111930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom
111963 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.49ms
111965 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof
111965 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130ns
111966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
114848 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
114848 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos
115772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos
115779 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms
115781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof
115781 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns
115782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
118595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
118595 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg
119531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg
119546 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.26ms
119551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof
119551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.51ns
119552 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
122323 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
122324 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos
123253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos
123268 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.82ms
123277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof
123277 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.3ns
123278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
126046 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
126047 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg
126970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg
126987 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms
126992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof
126992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns
126993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
129789 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
129789 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos
130714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos
130721 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms
130723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof
130723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.7ns
130724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
133570 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
133571 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg
134560 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg
134568 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms
134569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof
134569 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns
134570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
137370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
137371 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero
138339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero
138343 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms
138346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof
138346 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.81ns
138347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
141173 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
141174 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum
142189 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum
142199 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.87ms
142206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof
142206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.01ns
142210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
145030 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
145031 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom
145979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom
146017 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.67ms
146020 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof
146020 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.81ns
146022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
148814 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
148814 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos
149780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos
149800 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.75ms
149803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof
149803 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.91ns
149805 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
152718 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
152718 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg
153741 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg
153758 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.4ms
153760 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof
153760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.7ns
153761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
156615 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
156615 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos
157548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos
157568 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.39ms
157569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof
157569 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns
157570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
160463 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s
160463 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg
161404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg
161419 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.24ms
161420 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof
161420 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.6ns
161421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
164236 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
164237 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1
165165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1
165202 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.88ms
165205 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof
165205 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.71ns
165206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
168009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
168010 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2
168959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2
168962 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms
168964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof
168964 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.31ns
168965 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
171793 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
171793 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero
172743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero
172748 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms
172750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof
172750 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.01ns
172751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
175664 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
175664 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom
176620 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom
176628 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.33ms
176630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof
176630 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns
176631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
179454 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
179454 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos
180371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos
180379 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms
180380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof
180381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns
180381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
183140 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
183140 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg
184060 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg
184089 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.71ms
184095 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof
184096 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 627.32ns
184097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
186828 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
186829 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero
187744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero
187752 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.85ms
187753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof
187753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns
187754 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
190548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
190548 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero
191508 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero
191511 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms
191513 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof
191513 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns
191514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
194224 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s
194224 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum
195163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum
195167 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms
195168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof
195168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns
195169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
197946 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
197947 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom
198827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom
198831 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms
198839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof
198839 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns
198840 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
201801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
201801 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1
202706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1
202764 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.8ms
202766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof
202766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.4ns
202767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
205628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
205629 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2
206580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2
206656 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.28ms
206657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof
206658 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.4ns
206658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
209461 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
209461 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem
210364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem
210368 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms
210371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof
210371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.61ns
210373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
213187 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
213187 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod
214113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod
214144 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.94ms
214146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof
214146 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.71ns
214147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
216955 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
216955 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible
217819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible
217840 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.29ms
217842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof
217842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 111ns
217843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
220626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
220627 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep
221515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep
221518 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 941.02ns
221519 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof
221519 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns
221520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
224391 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
224391 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom
225279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom
225405 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.61ms
225411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof
225411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.5ns
225412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
228225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
228226 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero
229140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero
229150 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.91ms
229152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof
229152 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.41ns
229153 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
231974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
231974 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero
232918 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero
232924 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms
232925 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof
232926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns
232926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
235774 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
235774 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero
236691 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero
236705 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.55ms
236706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof
236707 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns
236707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
239444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
239445 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom
240353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom
240365 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.97ms
240367 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof
240367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns
240368 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
243144 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
243145 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty
244107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty
244110 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms
244112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof
244112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns
244113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
246850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
246850 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper
247767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper
247770 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms
247771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof
247772 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns
247772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
250495 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s
250495 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower
251387 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower
251402 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.46ms
251403 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof
251403 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns
251404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
254160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
254161 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds
255088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds
255100 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.29ms
255101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof
255101 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns
255102 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
257819 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s
257819 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2
258730 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2
258742 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.23ms
258744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof
258744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns
258744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
261503 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
261503 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2
262429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2
262432 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms
262434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof
262434 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns
262435 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
265255 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
265255 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete
266209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete
266212 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms
266213 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof
266213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns
266214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
269001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
269001 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2
269930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2
269934 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms
269936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof
269936 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns
269937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
272750 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
272750 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete
273695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete
273697 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms
273699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof
273699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns
273701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
276501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
276501 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete
277446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete
277448 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632.22ns
277450 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof
277450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns
277450 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
280208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
280208 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2
281126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2
281130 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms
281131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof
281131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns
281132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
283870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
283870 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete
284813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete
284816 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 740.22ns
284817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof
284818 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns
284818 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
287642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
287642 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive
288566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive
288616 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.4ms
288617 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof
288617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns
288618 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
291375 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
291375 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound
292304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound
292328 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.85ms
292329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof
292329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns
292330 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
295116 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
295116 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound
296121 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound
296147 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.25ms
296151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof
296151 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.11ns
296152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
299012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
299013 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element
299893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element
299955 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.2ms
299957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof
299957 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns
299958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
302688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
302689 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index
303577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index
303595 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.8ms
303597 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof
303597 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns
303597 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
306363 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
306364 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index
307241 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index
307275 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.1ms
307276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof
307276 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns
307277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
310073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
310074 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index
310963 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index
310981 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.42ms
310982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof
310982 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns
310983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
313761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
313761 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max
314663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max
314677 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.24ms
314678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof
314678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns
314679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
317429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
317429 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2
318314 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2
318330 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.47ms
318331 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof
318331 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns
318332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
321198 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
321198 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3
322127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3
322140 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.32ms
322141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof
322142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns
322142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
324924 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
324924 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4
325824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4
325843 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.02ms
325844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof
325845 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns
325845 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
328702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
328703 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max
329590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max
329610 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.28ms
329611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof
329611 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns
329612 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
332476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
332476 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2
333390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2
333408 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.67ms
333412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof
333412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.51ns
333413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
336227 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
336228 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3
337180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3
337198 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.28ms
337200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof
337200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns
337201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
340015 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
340015 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4
340926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4
340942 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.65ms
340943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof
340943 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns
340944 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
343689 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
343689 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0
344588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0
344605 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.87ms
344606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof
344606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns
344607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
347333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
347333 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt
348253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt
348270 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms
348271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof
348271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns
348272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
350987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s
350987 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete
351908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete
351914 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ms
351915 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof
351916 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns
351916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
354660 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
354660 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive
355588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive
355601 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.16ms
355603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof
355603 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns
355604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
358355 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
358355 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split
359258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split
359262 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms
359263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof
359263 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns
359264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
362116 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
362116 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0
363058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0
363060 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.62ns
363061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof
363061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns
363062 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
365803 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
365803 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1
366726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1
366729 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.42ns
366731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof
366731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.5ns
366732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
369465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
369465 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor
370401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor
370407 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms
370409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof
370409 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns
370409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
373160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
373161 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd
374091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd
374096 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms
374098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof
374098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns
374098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
376951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
376951 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono
377879 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono
377889 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ms
377890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof
377890 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns
377891 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
380745 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
380746 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete
381716 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete
381719 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms
381720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof
381721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns
381721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
384573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
384574 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight
385579 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight
385582 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 571.32ns
385585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof
385585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.41ns
385586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
388481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
388482 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive
389480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive
389485 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms
389487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof
389487 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns
389487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
392377 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s
392377 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete
393304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete
393307 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 593.01ns
393308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof
393308 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns
393309 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
396125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
396125 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete
397029 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete
397031 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 521.41ns
397033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof
397033 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns
397033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
399808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
399808 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower
400704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower
400706 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 521.31ns
400708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof
400708 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns
400708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
403446 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
403447 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper
404383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper
404387 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms
404388 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof
404388 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns
404389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
407143 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
407143 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete
408091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete
408105 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ms
408106 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof
408106 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns
408107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
410903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
410903 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete
411773 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete
411777 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms
411778 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof
411778 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns
411779 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
414586 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
414586 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct
415502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct
415508 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms
415510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof
415510 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.11ns
415511 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
418356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
418356 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete
419240 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete
419244 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms
419247 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof
419247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.9ns
419248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
421981 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
421981 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity
422860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity
422875 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms
422878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof
422878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns
422879 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
425791 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
425791 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete
426720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete
426723 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms
426725 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof
426725 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns
426725 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
429546 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
429546 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity
430426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity
430429 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms
430430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof
430430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns
430431 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
433203 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
433204 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete
434133 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete
434136 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms
434137 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof
434138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns
434138 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
436897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
436897 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive
437807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive
437821 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.22ms
437822 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof
437823 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns
437823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
440544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s
440544 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete
441505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete
441510 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 365.91ns
441512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof
441512 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns
441513 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
444305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
444305 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono
445234 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono
445264 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.14ms
445265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof
445266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns
445266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
448073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
448073 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete
449014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete
449018 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms
449019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof
449019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns
449020 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
451794 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
451794 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess
452731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess
452748 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms
452751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof
452751 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.71ns
452752 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
455535 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
455535 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2
456444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2
456467 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.4ms
456469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof
456469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns
456469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
459249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
459250 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow
460173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow
460193 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.23ms
460194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof
460194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns
460195 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
462950 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
462950 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete
463864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete
463867 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.52ns
463868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof
463868 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns
463869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
466656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
466657 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze
467583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze
467588 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms
467590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof
467590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns
467590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
470302 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s
470303 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals
471229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals
471232 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms
471235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof
471235 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.91ns
471236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
474035 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
474035 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1
474959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1
474962 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 887.12ns
474965 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof
474966 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.01ns
474967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
477805 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
477805 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2
478743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2
478746 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 852.12ns
478747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof
478747 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns
478748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
481653 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
481653 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1
482619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1
482622 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms
482623 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof
482623 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns
482624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
485403 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
485403 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2
486358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2
486361 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms
486362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof
486362 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns
486363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
489183 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
489183 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges
490104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges
490112 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms
490113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof
490113 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns
490114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
492849 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
492849 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1
493799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1
493806 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms
493807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof
493807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns
493808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
496539 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
496539 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2
497473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2
497480 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ms
497481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof
497481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns
497482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
500266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
500266 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition
501249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition
501257 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.42ms
501258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof
501258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns
501259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
504071 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
504071 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue
505079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue
505083 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms
505085 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof
505086 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.81ns
505086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
508057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
508057 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny
509007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny
509011 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms
509012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof
509012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns
509013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
511789 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
511789 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast
512783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast
512786 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.52ns
512787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof
512787 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns
512787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
515618 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
515618 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton
516589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton
516592 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 959.83ns
516593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof
516593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns
516594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
519337 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
519338 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete
520277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete
520279 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 773.22ns
520280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof
520280 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns
520281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
523016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
523016 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat
523971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat
523980 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.72ms
523981 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof
523981 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns
523982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
526754 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
526754 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub
527702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub
527705 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms
527706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof
527706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns
527707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
530412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s
530412 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse
531365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse
531371 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms
531372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof
531372 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns
531373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
534134 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
534134 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty
535081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty
535083 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 932.92ns
535085 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof
535085 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns
535085 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
537885 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
537885 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton
538846 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton
538849 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.32ns
538850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof
538850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns
538851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
541658 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
541658 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat
542596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat
542599 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms
542600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof
542600 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns
542601 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
545361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
545361 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub
546311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub
546314 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 739.82ns
546315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof
546315 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns
546316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
549217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
549217 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse
550198 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse
550201 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms
550202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof
550202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns
550203 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
553047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
553047 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft
553992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft
553994 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 998.33ns
553995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof
553995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns
553996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
556752 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
556752 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight
557644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight
557648 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms
557650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof
557650 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns
557650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
560405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
560405 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ
561365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ
561368 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 934.42ns
561369 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof
561369 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns
561370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
564184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
564184 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ
565148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ
565157 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.85ms
565158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof
565158 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns
565159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
568022 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
568022 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ
568994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ
568996 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 565.01ns
568997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof
568997 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns
568998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
571843 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
571843 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ
572816 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ
572822 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms
572823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof
572823 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns
572824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
575657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
575657 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ
576583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ
576586 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms
576587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof
576587 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns
576588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
579381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
579381 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ
580304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ
580307 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 687.22ns
580308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof
580308 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns
580309 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
583075 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
583075 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ
584025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ
584029 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms
584030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof
584030 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns
584031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
586783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
586783 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ
587716 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ
587718 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 971.23ns
587720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof
587720 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns
587721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
590463 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
590463 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ
591407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ
591410 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms
591411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof
591411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns
591412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
594178 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
594179 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ
595118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ
595121 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms
595122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof
595122 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns
595123 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
597958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
597958 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ
598906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ
598910 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms
598911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof
598911 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns
598912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
601682 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
601682 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1
602627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1
602636 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.11ms
602637 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof
602638 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 717.32ns
602638 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
605388 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
605388 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2
606324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2
606332 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms
606334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof
606334 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns
606334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
609167 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
609167 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty
610096 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty
610103 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms
610104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof
610104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns
610105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
612970 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
612970 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete
613944 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete
613951 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms
613955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof
613955 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns
613956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
616785 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
616785 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR
617732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR
617743 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.45ms
617744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof
617744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns
617745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
620537 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
620537 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL
621513 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL
621524 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms
621525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof
621525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns
621526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
624571 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s
624571 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR
625511 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR
625521 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.54ms
625523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof
625523 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns
625524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
628370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
628371 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL
629278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL
629286 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms
629287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof
629287 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns
629288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
632102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
632103 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split
633063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split
633084 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.76ms
633086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof
633086 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns
633086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
635912 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
635912 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper
636856 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper
636880 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.62ms
636881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof
636881 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns
636882 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
639709 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
639709 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete
640630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete
640650 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.16ms
640651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof
640652 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns
640652 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
643551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
643552 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower
644557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower
644583 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.54ms
644585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof
644585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns
644586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
647410 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
647410 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete
648346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete
648366 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ms
648367 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof
648367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns
648368 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
651097 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
651098 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three
651990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three
652045 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.48ms
652047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof
652047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns
652048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
654814 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
654814 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty
655720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty
655724 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms
655726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof
655726 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns
655727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
658621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s
658621 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand
659580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand
659585 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms
659587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof
659588 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.11ns
659588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
662358 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
662358 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper
663267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper
663270 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms
663271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof
663272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns
663272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
666027 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
666028 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq
666964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq
666978 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.76ms
666980 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof
666980 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns
666980 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
669734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
669734 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2
670673 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2
670680 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms
670681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof
670681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns
670682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
673462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
673462 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton
674377 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton
674380 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms
674381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof
674381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns
674382 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
677068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s
677068 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst
677997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst
678007 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.42ms
678008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof
678008 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns
678009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
680801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
680801 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond
681751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond
681761 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.08ms
681762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof
681762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns
681763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
684701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
684701 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub
685679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub
685694 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.87ms
685696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof
685696 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns
685697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
688619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s
688619 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq
689568 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq
689571 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms
689574 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof
689574 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns
689574 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
692445 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
692445 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq
693419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq
693423 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms
693424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof
693424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns
693425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
696203 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
696203 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq
697144 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq
697150 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms
697151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof
697151 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns
697152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
700160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s
700160 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv
701132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv
701137 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms
701138 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof
701138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns
701139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
704027 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s
704028 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange
705018 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange
705064 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.67ms
705066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof
705066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns
705067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
707923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
707923 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans
708846 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans
708865 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.1ms
708867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof
708867 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.31ns
708868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
711644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
711644 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl
712587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl
712599 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.77ms
712600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof
712600 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns
712601 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
715418 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
715418 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit
716398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit
716401 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 538.71ns
716403 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof
716403 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.51ns
716404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
719346 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
719346 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight
720271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight
720360 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.03ms
720363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof
720363 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns
720364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
723145 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
723145 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap
724057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap
724093 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.53ms
724094 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof
724094 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns
724095 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
726800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s
726800 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0
727719 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0
727721 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 197.41ns
727723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof
727723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns
727723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
730469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
730469 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1
731419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1
731421 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 219.31ns
731422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof
731422 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns
731423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
734185 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
734185 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2
735103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2
735104 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 238.71ns
735106 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof
735106 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns
735107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
737853 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
737853 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3
738780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3
738782 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 361.21ns
738783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof
738783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns
738784 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
741606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
741606 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall
742552 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall
742687 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 132.39ms
742692 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof
742693 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.71ns
742694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
745479 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
745479 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists
746414 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists
746463 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.57ms
746465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof
746465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns
746470 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
749353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
749353 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2
750313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2
750315 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns
750344 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
750399 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight'
750426 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight'
750433 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop'
750441 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft''
750445 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft''
750446 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft''
750449 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
750452 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqNPermRange'
750454 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1'
750459 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft'
750460 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch'
750702 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft'
750704 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft'
750706 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1'
750707 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft'
750708 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch'
750845 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft'
750846 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft'
750849 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft'
750851 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2'
750853 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft'
750853 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch'
751020 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft'
751021 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
751023 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
751024 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2'
751025 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft'
751029 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch'
751149 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft'
751151 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
751153 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
751153 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1'
751154 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft'
751155 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch'
751163 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft'
751164 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
751165 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0'
751167 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1'
751169 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft'
751170 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch'
751179 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft'
751180 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft'
751181 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0'
751182 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv with='v_x_0''
751183 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft'
751184 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch'
751307 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv with='v_y_0''
751308 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft'
751310 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch'
751426 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0''
751430 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)''
751434 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight'
751436 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight'
751437 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight'
751438 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight'
751439 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap'
751442 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
751448 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm'
751449 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1'
751450 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0''
751451 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft'
751452 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch'
751562 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
751565 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight'
751567 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight'
751568 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft'
751570 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0''
751571 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft'
751573 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch'
751698 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap'
751700 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated'
751701 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0'
751703 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft'
751704 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft'
751704 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft'
751706 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0'
751707 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch'
751803 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0'
751805 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch'
751905 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch'
751910 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch'
751914 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap'
751916 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated'
751917 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0'
751918 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft'
751918 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft'
751919 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft'
751920 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0'
751921 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch'
751930 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch'
751934 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch'
752102 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap'
752104 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated'
752105 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0'
752106 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft'
752106 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft'
752107 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft'
752108 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0'
752109 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch'
752178 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch'
752183 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch'
752275 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]''
752276 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective'
752278 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0''
752280 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0''
752281 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft'
752281 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch'
752400 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch'
752404 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0''
752405 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)''
752406 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight'
752407 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight'
752408 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight'
752409 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight'
752410 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch'
752418 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm'
752419 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0''
752420 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1''
752422 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch'
752512 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight'
752513 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight'
752514 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft'
752515 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0''
752516 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft'
752516 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch'
752611 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap'
752612 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated'
752613 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0'
752615 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft'
752615 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft'
752616 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft'
752617 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0'
752623 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch'
752709 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0'
752710 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch'
752782 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0''
752782 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft'
752783 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch'
752787 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch'
752791 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch'
752795 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch'
752914 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap'
752915 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated'
752916 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0'
752917 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch'
752927 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch'
753009 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch'
756613 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 149: 'cut '(int)s_0[v_y_0] = v_y_0''
756614 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)''
756621 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight'
756622 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight'
756622 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight'
756623 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight'
756624 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch'
756632 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm'
756633 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0''
756635 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0''
756635 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft'
756636 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch'
756733 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch'
756737 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight'
756738 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight'
756739 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft'
756740 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0''
756741 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft'
756741 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch'
756838 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap'
756840 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated'
756841 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0'
756842 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft'
756843 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft'
756844 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft'
756845 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0'
756847 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch'
756923 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0'
756924 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch'
756997 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch'
757001 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch'
757006 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap'
757007 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated'
757008 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0'
757009 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch'
757018 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch'
757148 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap'
757149 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated'
757150 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0'
757151 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch'
757220 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch'
757229 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0''
757229 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)''
757231 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight'
757232 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight'
757232 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight'
757233 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight'
757233 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch'
757244 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm'
757245 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0''
757246 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0''
757246 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft'
757247 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch'
757333 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))''
757335 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0''
757341 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0''
757341 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft'
757342 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch'
757435 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch'
757440 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight'
757441 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight'
757442 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft'
757442 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0''
757443 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft'
757443 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch'
757544 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap'
757546 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated'
757546 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0'
757548 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft'
757548 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft'
757549 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft'
757549 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0'
757550 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap'
757551 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated'
757552 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0'
757553 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft'
757553 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft'
757554 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft'
757554 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0'
757555 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch'
757654 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0'
757656 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch'
757662 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch'
757742 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch'
757825 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split'
757826 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap'
757827 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated'
757829 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0'
757830 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft'
757831 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft'
757831 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft'
757832 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0'
757833 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch'
757838 WARN Test worker d.u.i.k.p.i.ApplyStrategy doWork exception java.lang.AssertionError: Formula Term top level of equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,jv_0),int::seqGet(s_0,v_x_0),if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))) does not exist
at de.uka.ilkd.key.strategy.BuiltInRuleAppContainer.<init>(BuiltInRuleAppContainer.java:42)
757839 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch'
757839 WARN Test worker d.u.i.k.p.i.ApplyStrategy doWork exception java.lang.AssertionError: Formula Term top level of equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,jv_0),int::seqGet(s_0,v_x_0),if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))) does not exist
at de.uka.ilkd.key.strategy.BuiltInRuleAppContainer.<init>(BuiltInRuleAppContainer.java:42)
757841 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch'
757842 WARN Test worker d.u.i.k.p.i.ApplyStrategy doWork exception java.lang.AssertionError: Formula Term top level of equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,jv_0),int::seqGet(s_0,v_x_0),if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))) does not exist
at de.uka.ilkd.key.strategy.BuiltInRuleAppContainer.<init>(BuiltInRuleAppContainer.java:42)
757843 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap'
757843 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine GOALS: 8
757844 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),exists{v_r:Seq}(and(and(and(and(equals(seqLen(v_r),seqLen(f_s)),seqNPerm(v_r)),all{v_iv:int}(imp(and(leq(Z(0(#)),v_iv),lt(v_iv,seqLen(f_s))),equals(any::seqGet(f_s,v_iv),any::seqGet(f_t,int::seqGet(v_r,v_iv)))))),equals(int::seqGet(v_r,v_x_0),v_x_0)),equals(int::seqGet(v_r,v_y_0),v_y_0)))]
757848 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(int::seqGet(seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0),v_y_0),v_y_0)]
757848 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(int::seqGet(seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0),v_x_0),v_x_0)]
757849 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),and(and(and(leq(Z(0(#)),jv_0),leq(Z(0(#)),v_y_0)),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0)))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0)))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(seqSwap(s_0,jv_0,v_x_0),v_iv_0)))]
757849 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),equals(v_iv_0,v_y_0),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(seqSwap(s_0,jv_0,v_x_0),v_iv_0)))]
757849 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [equals(v_iv_0,v_y_0),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),and(and(and(leq(Z(0(#)),jv_0),leq(Z(0(#)),v_x_0)),lt(jv_0,seqLen(s_0))),lt(v_x_0,seqLen(s_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,jv_0)))]
757849 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [equals(jv_0,jv_0),lt(v_x_0,seqLen(s_0)),equals(v_iv_0,v_y_0),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0)))]
757849 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [lt(v_x_0,seqLen(s_0)),equals(v_iv_0,v_y_0),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),equals(jv_0,jv_0),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))]
757860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof
757860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns
757861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
760983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s
760983 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1
761971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1
761972 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns
761973 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
761981 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)''
761994 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x''
761996 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y''
761997 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft'
761998 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch'
762002 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft'
762004 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
762010 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1'
762013 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight'
762013 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch'
762024 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0''
762028 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight'
762029 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch'
762080 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight'
762081 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight'
762082 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0''
762083 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft'
762083 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch'
762157 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft'
762157 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange'
762159 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0''
762159 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft'
762160 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch'
762164 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
762165 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
762166 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange'
762167 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x''
762168 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft'
762168 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch'
762257 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
762258 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
762259 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange'
762260 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y''
762261 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft'
762262 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch'
762356 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
762357 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft'
762358 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0'
762359 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef'
762360 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0'
762361 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0'
762361 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0'
762362 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2'
762363 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft'
762364 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0'
762364 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0'
762365 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0'
762366 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0'
762366 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0'
762367 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0'
762368 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0'
762369 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0'
762370 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0'
762371 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch'
762374 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch'
762408 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0'
762410 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
762472 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0'
762473 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective'
762475 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0''
762476 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y''
762477 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft'
762477 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
762534 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch'
762536 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0'
762538 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective'
762539 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0''
762541 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x''
762541 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft'
762543 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch'
762598 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch'
762601 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch'
762604 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch'
762661 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch'
762724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof
762725 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.11ns
762726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
765575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
765575 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq
766572 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq
766601 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.38ms