834 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key
852 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.81ms
1044 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1059 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)
1949 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1953 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1957 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1957 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
3286 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
8242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.2s
8305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key
8336 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.5ns
8349 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof
8349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.9ns
8353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
11143 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
11146 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut
12092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut
12116 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.37ms
12125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof
12125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.3ns
12127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
14757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s
14758 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight
15613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight
15628 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.88ms
15631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof
15631 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.31ns
15633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
18249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s
18249 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1
19107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1
19114 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms
19117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof
19117 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.4ns
19118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
21601 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s
21602 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2
22469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2
22482 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ms
22486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof
22487 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 619.01ns
22489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
24967 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s
24967 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos
25780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos
25820 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.7ms
25823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof
25823 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.3ns
25824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
28284 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
28284 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg
29115 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg
29135 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.62ms
29138 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof
29138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns
29139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
31561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
31561 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt
32364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt
32367 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 783.01ns
32369 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof
32369 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.9ns
32370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
34784 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
34785 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong
35588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong
35590 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.61ns
35592 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof
35592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.9ns
35593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
38018 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
38019 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort
38832 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort
38835 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.21ns
38838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof
38838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.4ns
38840 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
41237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s
41238 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte
42031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte
42034 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.2ns
42037 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof
42037 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.3ns
42038 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
44425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
44426 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar
45211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar
45214 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.31ns
45217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof
45218 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.9ns
45219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
47604 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
47604 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1
48388 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1
48428 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.05ms
48430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof
48430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.4ns
48431 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
50818 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
50818 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2
51603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2
51673 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.33ms
51682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof
51683 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.16ms
51685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
54087 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s
54088 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists
54877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists
55079 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.8ms
55084 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof
55084 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.61ns
55086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
57492 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
57493 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one
58281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one
58285 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms
58288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof
58288 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.7ns
58289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
60699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
60700 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one
61491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one
61494 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms
61498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof
61498 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 376ns
61499 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
63908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
63908 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero
64707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero
64758 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.64ms
64762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof
64762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns
64763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
67170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
67171 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1
67954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1
67969 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.93ms
67971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof
67971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.2ns
67972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
70373 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s
70373 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2
71165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2
71178 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.82ms
71180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof
71180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.8ns
71181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
73589 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
73589 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1
74381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1
74397 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.08ms
74401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof
74401 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.91ns
74402 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
76812 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
76812 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2
77598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2
77612 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.44ms
77615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof
77615 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.9ns
77616 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
80003 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
80004 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1
80788 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1
80818 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.38ms
80819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof
80819 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.7ns
80820 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
83218 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s
83218 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2
84008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2
84011 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms
84012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof
84012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.9ns
84013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
86399 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
86399 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom
87186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom
87223 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.34ms
87225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof
87225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.7ns
87226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
89612 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
89612 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus
90407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus
90461 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.17ms
90465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof
90465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.11ns
90467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
92874 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
92874 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom
93632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom
93704 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.45ms
93706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof
93706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.8ns
93707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
96089 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
96089 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos
96843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos
96850 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms
96853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof
96853 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns
96854 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
99249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s
99250 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg
100002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg
100015 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.87ms
100016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof
100017 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns
100017 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
102410 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
102410 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos
103163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos
103174 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ms
103175 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof
103175 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns
103176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
105580 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s
105580 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg
106332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg
106340 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms
106342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof
106342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.8ns
106343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
108738 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
108738 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos
109546 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos
109556 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms
109560 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof
109561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.8ns
109562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
111970 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
111970 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg
112726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg
112733 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.88ms
112735 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof
112735 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns
112736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
115126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
115126 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero
115876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero
115880 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms
115881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof
115881 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns
115882 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
118295 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
118296 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum
119056 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum
119078 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.54ms
119079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof
119080 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns
119081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
121470 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
121470 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom
122249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom
122306 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.29ms
122309 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof
122310 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 624.51ns
122319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
124695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
124696 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos
125477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos
125496 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.72ms
125501 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof
125501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 548.11ns
125503 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
127873 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
127873 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg
128648 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg
128666 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.39ms
128667 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof
128667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns
128668 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
131037 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
131037 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos
131817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos
131835 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.05ms
131836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof
131836 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns
131837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
134200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
134200 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg
134983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg
135000 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.91ms
135001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof
135001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns
135002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
137361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
137361 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1
138134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1
138173 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.35ms
138175 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof
138175 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns
138176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
140541 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
140541 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2
141315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2
141317 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms
141318 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof
141319 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns
141319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
143676 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
143676 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero
144450 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero
144454 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms
144456 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof
144456 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns
144456 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
146820 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
146820 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom
147598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom
147606 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms
147607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof
147608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns
147608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
149974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
149974 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos
150750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos
150759 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ms
150761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof
150761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.1ns
150762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
153127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
153128 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg
153901 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg
153920 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.13ms
153921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof
153921 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns
153922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
156280 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
156281 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero
157056 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero
157065 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.36ms
157070 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof
157071 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.3ns
157072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
159435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
159435 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero
160217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero
160220 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms
160222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof
160222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.3ns
160223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
162592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
162593 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum
163371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum
163379 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.31ms
163381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof
163381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.9ns
163382 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
165750 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
165750 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom
166522 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom
166527 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms
166528 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof
166528 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns
166529 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
168892 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
168893 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1
169665 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1
169740 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.94ms
169742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof
169742 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299ns
169744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
172104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
172105 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2
172877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2
172963 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.21ms
172965 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof
172965 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns
172966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
175325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
175326 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem
176100 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem
176104 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms
176106 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof
176107 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.6ns
176108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
178482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
178482 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod
179260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod
179317 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.55ms
179319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof
179324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.87ms
179325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
181690 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
181690 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible
182463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible
182494 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.08ms
182495 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof
182495 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns
182496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
184866 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
184866 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep
185640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep
185643 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms
185645 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof
185645 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.5ns
185646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
188014 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
188015 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom
188791 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom
188938 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 135.59ms
188940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof
188940 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns
188941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
191322 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
191322 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero
192096 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero
192108 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.64ms
192109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof
192109 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns
192110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
194509 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s
194509 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero
195289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero
195310 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.81ms
195311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof
195311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns
195312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
197677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
197677 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero
198448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero
198465 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms
198466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof
198466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns
198467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
200829 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
200830 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom
201606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom
201623 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.27ms
201626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof
201626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns
201626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
203983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
203983 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty
204753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty
204756 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms
204757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof
204757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns
204758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
207111 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
207112 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper
207863 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper
207867 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms
207869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof
207869 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns
207869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
210260 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
210260 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower
211012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower
211036 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21ms
211037 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof
211037 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns
211038 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
213434 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s
213434 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds
214184 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds
214201 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.61ms
214202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof
214202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns
214203 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
216582 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
216582 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2
217330 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2
217345 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.88ms
217346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof
217346 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns
217347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
219719 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
219719 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2
220467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2
220471 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms
220472 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof
220472 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns
220473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
222856 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
222856 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete
223603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete
223608 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms
223610 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof
223610 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.6ns
223611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
225990 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
225990 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2
226738 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2
226743 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms
226744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof
226744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns
226745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
229124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
229125 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete
229877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete
229880 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms
229881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof
229881 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns
229882 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
232266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
232267 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete
233016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete
233019 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.31ns
233021 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof
233021 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.2ns
233022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
235382 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
235383 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2
236163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2
236167 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms
236168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof
236168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns
236169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
238536 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
238536 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete
239313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete
239316 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 992.61ns
239317 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof
239317 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns
239318 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
241682 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
241683 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive
242454 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive
242500 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.09ms
242503 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof
242503 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.8ns
242504 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
244867 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
244867 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound
245638 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound
245672 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.61ms
245673 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof
245673 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns
245674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
248051 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
248052 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound
248823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound
248852 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.38ms
248853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof
248853 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns
248854 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
251220 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
251221 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element
251994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element
252036 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.76ms
252038 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof
252038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.2ns
252039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
254395 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
254396 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index
255169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index
255197 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.21ms
255198 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof
255198 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns
255199 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
257555 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
257555 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index
258330 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index
258377 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.68ms
258379 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof
258379 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns
258380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
260740 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
260741 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index
261513 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index
261541 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.48ms
261542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof
261542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns
261543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
263898 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
263898 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max
264680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max
264699 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.47ms
264700 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof
264701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns
264701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
267062 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
267062 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2
267837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2
267863 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.59ms
267866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof
267866 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230ns
267867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
270223 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
270223 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3
270997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3
271017 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms
271018 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof
271018 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns
271019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
273374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
273374 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4
274148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4
274175 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.46ms
274176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof
274176 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns
274177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
276537 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
276537 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max
277312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max
277337 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.19ms
277338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof
277338 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns
277339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
279701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
279701 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2
280476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2
280500 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.71ms
280502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof
280502 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns
280503 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
282859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
282859 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3
283635 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3
283660 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.96ms
283661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof
283661 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns
283662 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
286029 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
286029 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4
286802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4
286823 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.03ms
286824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof
286824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns
286825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
289184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
289184 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0
289955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0
289980 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.73ms
289981 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof
289981 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns
289982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
292343 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
292343 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt
293119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt
293143 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.79ms
293145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof
293145 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns
293145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
295540 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
295540 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete
296313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete
296321 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms
296322 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof
296322 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns
296323 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
298684 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
298684 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive
299458 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive
299476 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.44ms
299478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof
299478 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns
299479 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
301840 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
301840 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split
302613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split
302617 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms
302618 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof
302618 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns
302619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
304978 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
304978 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0
305749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0
305751 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.61ns
305752 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof
305752 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns
305753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
308103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
308103 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1
308874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1
308877 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 767.11ns
308878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof
308878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns
308879 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
311248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
311248 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor
312019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor
312027 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.88ms
312029 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof
312029 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.1ns
312030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
314390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
314391 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd
315168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd
315175 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms
315177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof
315177 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.1ns
315178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
317535 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
317535 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono
318311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono
318323 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.55ms
318325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof
318325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns
318325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
320682 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
320682 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete
321432 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete
321436 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms
321438 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof
321438 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns
321438 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
323808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
323809 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight
324557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight
324559 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 567.21ns
324561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof
324561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.1ns
324562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
326929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
326929 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive
327679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive
327687 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms
327689 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof
327689 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.8ns
327690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
330067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
330067 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete
330815 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete
330817 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 676.41ns
330819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof
330819 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns
330819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
333200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
333201 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete
333950 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete
333952 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.51ns
333953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof
333953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns
333954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
336326 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
336326 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower
337073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower
337075 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.21ns
337076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof
337076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns
337077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
339452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
339452 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper
340202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper
340206 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms
340207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof
340207 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns
340208 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
342587 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
342587 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete
343341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete
343350 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.05ms
343352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof
343352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns
343352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
345705 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
345705 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete
346477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete
346481 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms
346482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof
346483 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns
346483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
348840 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
348841 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct
349613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct
349620 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms
349621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof
349621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns
349622 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
351975 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
351975 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete
352747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete
352751 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms
352753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof
352753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns
352753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
355114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
355114 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity
355886 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity
355902 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.78ms
355903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof
355903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns
355904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
358264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
358264 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete
359043 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete
359047 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms
359050 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof
359050 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 192ns
359051 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
361406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
361406 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity
362181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity
362184 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms
362185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof
362185 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns
362186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
364536 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
364536 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete
365307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete
365311 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms
365312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof
365312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns
365313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
367660 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
367660 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive
368431 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive
368450 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.83ms
368452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof
368452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns
368452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
370808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
370809 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete
371583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete
371588 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 753.31ns
371591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof
371591 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.1ns
371592 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
373937 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
373937 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono
374703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono
374742 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.13ms
374743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof
374743 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns
374744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
377104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
377104 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete
377877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete
377881 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms
377882 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof
377882 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns
377883 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
380232 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
380232 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess
381003 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess
381025 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.74ms
381026 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof
381026 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns
381027 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
383380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
383380 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2
384150 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2
384171 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.99ms
384172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof
384172 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns
384173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
386541 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
386541 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow
387316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow
387340 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.05ms
387341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof
387341 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns
387342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
389706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
389706 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete
390481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete
390484 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.01ns
390485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof
390485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns
390486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
392851 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
392851 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze
393624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze
393630 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms
393631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof
393631 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns
393632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
395989 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
395989 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals
396770 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals
396774 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms
396776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof
396776 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.2ns
396777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
399156 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
399156 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1
399931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1
399934 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 871.11ns
399935 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof
399935 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.49ns
399936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
402290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
402291 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2
403066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2
403069 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 936.91ns
403071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof
403071 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.7ns
403071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
405428 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
405428 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1
406205 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1
406209 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms
406210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof
406210 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns
406211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
408567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
408568 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2
409347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2
409350 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms
409351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof
409351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns
409352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
411708 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
411708 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges
412485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges
412494 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.23ms
412497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof
412497 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns
412498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
414860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
414860 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1
415639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1
415651 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ms
415652 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof
415652 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns
415653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
418003 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
418003 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2
418786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2
418797 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.83ms
418798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof
418798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns
418799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
421150 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
421150 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition
421933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition
421945 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ms
421946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof
421946 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns
421947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
424298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
424299 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue
425082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue
425087 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms
425088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof
425088 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns
425089 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
427439 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
427439 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny
428217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny
428223 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms
428224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof
428224 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns
428225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
430575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
430575 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast
431354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast
431356 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.71ns
431357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof
431357 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns
431358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
433719 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
433719 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton
434497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton
434500 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms
434501 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof
434501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns
434502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
436853 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
436853 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete
437632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete
437634 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 842.51ns
437637 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof
437637 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233ns
437638 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
440004 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
440004 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat
440783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat
440793 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms
440795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof
440795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns
440795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
443152 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
443152 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub
443931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub
443935 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms
443936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof
443936 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns
443937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
446286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
446287 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse
447065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse
447072 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms
447074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof
447074 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.2ns
447075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
449432 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
449432 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty
450213 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty
450215 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.61ns
450216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof
450216 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns
450217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
452562 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s
452562 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton
453341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton
453343 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.51ns
453344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof
453344 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns
453345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
455689 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s
455689 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat
456467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat
456471 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms
456472 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof
456472 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns
456473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
458819 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
458819 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub
459601 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub
459604 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms
459606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof
459606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.4ns
459607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
461961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
461961 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse
462741 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse
462744 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms
462745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof
462745 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns
462746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
465119 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
465119 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft
465878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft
465880 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms
465882 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof
465882 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns
465882 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
468255 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
468255 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight
469012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight
469017 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms
469018 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof
469018 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns
469019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
471390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
471390 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ
472146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ
472149 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms
472150 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof
472150 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns
472151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
474518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
474518 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ
475298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ
475309 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.41ms
475311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof
475311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.9ns
475312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
477660 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
477661 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ
478440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ
478442 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.61ns
478443 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof
478443 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns
478444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
480792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
480792 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ
481577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ
481584 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms
481585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof
481585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns
481586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
483931 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
483931 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ
484710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ
484712 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 908.51ns
484714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof
484714 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns
484714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
487059 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s
487060 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ
487840 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ
487842 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 809.51ns
487844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof
487844 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns
487844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
490220 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
490221 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ
490978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ
490983 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms
490984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof
490984 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns
490985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
493374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
493374 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ
494154 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ
494157 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms
494159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof
494160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.5ns
494160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
496518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
496518 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ
497297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ
497301 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms
497303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof
497303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns
497304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
499659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
499659 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ
500442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ
500446 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms
500448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof
500448 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns
500449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
502802 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
502802 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ
503585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ
503589 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms
503591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof
503592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns
503592 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
505961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
505961 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1
506718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1
506732 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.17ms
506733 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof
506733 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns
506734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
509099 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
509099 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2
509878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2
509893 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms
509895 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof
509895 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns
509896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
512246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
512246 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty
513033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty
513043 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms
513044 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof
513044 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns
513045 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
515391 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
515391 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete
516173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete
516186 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.68ms
516187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof
516187 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns
516188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
518562 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
518562 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR
519319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR
519345 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.02ms
519346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof
519346 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns
519347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
521718 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
521718 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL
522499 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL
522524 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.71ms
522526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof
522526 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns
522526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
524874 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
524875 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR
525654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR
525677 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.89ms
525678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof
525678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns
525679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
528020 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s
528020 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL
528800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL
528814 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms
528815 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof
528816 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns
528816 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
531190 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
531190 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split
531969 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split
531999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.38ms
532001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof
532001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns
532002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
534354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
534355 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper
535136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper
535183 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.65ms
535184 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof
535184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns
535185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
537538 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
537538 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete
538320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete
538357 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.06ms
538359 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof
538359 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns
538360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
540724 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
540724 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower
541505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower
541546 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.98ms
541548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof
541548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns
541549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
543897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
543897 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete
544679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete
544722 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.21ms
544724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof
544724 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns
544725 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
547093 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
547093 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three
547850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three
547967 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 110.05ms
547968 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof
547969 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns
547969 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
550343 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
550343 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty
551125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty
551133 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.85ms
551134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof
551135 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns
551135 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
553477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s
553477 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand
554256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand
554264 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms
554265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof
554265 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns
554266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
556631 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
556631 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper
557390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper
557395 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms
557396 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof
557396 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns
557397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
559764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
559764 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq
560545 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq
560563 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.09ms
560565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof
560565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns
560565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
562906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s
562906 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2
563687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2
563700 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.37ms
563701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof
563701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns
563702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
566073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
566073 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton
566852 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton
566855 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms
566856 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof
566856 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns
566857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
569204 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
569204 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst
569986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst
570003 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.96ms
570004 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof
570004 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns
570005 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
572380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
572380 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond
573167 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond
573183 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.74ms
573185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof
573185 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns
573186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
575532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
575533 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub
576314 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub
576333 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.05ms
576334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof
576334 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns
576335 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
578703 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
578703 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq
579462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq
579465 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms
579466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof
579466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns
579467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
581834 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
581834 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq
582614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq
582617 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms
582618 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof
582618 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns
582619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
584970 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
584970 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq
585754 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq
585761 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms
585762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof
585762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns
585762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
588146 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
588146 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv
588926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv
588932 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms
588933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof
588933 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns
588934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
591284 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
591284 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange
592066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange
592137 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.9ms
592138 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof
592138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns
592139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
594525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
594525 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans
595305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans
595331 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.17ms
595332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof
595332 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns
595333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
597704 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
597704 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl
598463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl
598485 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.27ms
598486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof
598486 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns
598487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
600854 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
600854 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit
601641 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit
601643 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 280.6ns
601645 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof
601645 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns
601646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
604026 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
604026 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight
604786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight
605019 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.64ms
605021 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof
605021 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns
605022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
607376 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
607376 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap
608160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap
608209 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.27ms
608211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof
608211 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns
608211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
610590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
610590 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0
611372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0
611374 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 374ns
611378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof
611378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234ns
611379 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
613735 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
613736 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1
614518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1
614520 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 348.11ns
614521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof
614521 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns
614522 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
616883 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
616883 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2
617661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2
617663 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 362.11ns
617664 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof
617664 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns
617665 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
620033 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
620033 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3
620793 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3
620795 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 512.51ns
620796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof
620796 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns
620797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
623160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
623160 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall
623941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall
624051 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.17ms
624053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof
624053 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.4ns
624054 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
626442 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
626442 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists
627224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists
627276 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.43ms
627277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof
627277 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns
627279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
629654 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
629654 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2
630436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2
630438 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns
630467 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
630513 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight'
630535 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight'
630543 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop'
630551 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft''
630553 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft''
630554 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft''
630557 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
630560 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqNPermRange'
630562 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1'
630566 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft'
630567 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch'
630778 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft'
630779 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft'
630780 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1'
630781 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft'
630782 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch'
630902 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft'
630903 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft'
630906 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft'
630909 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2'
630910 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft'
630911 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch'
631058 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft'
631060 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
631061 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
631062 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2'
631063 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft'
631067 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch'
631169 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft'
631171 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
631172 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
631173 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1'
631174 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft'
631175 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch'
631181 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft'
631182 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
631183 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0'
631185 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1'
631186 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft'
631187 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch'
631193 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft'
631195 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft'
631196 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0'
631197 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv with='v_x_0''
631198 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft'
631199 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch'
631311 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv with='v_y_0''
631312 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft'
631314 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch'
631413 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0''
631414 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)''
631417 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight'
631418 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight'
631419 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight'
631421 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight'
631422 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap'
631424 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
631428 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm'
631430 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1'
631431 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0''
631431 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft'
631432 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch'
631557 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
631560 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight'
631562 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight'
631563 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft'
631564 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0''
631565 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft'
631567 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch'
631667 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap'
631669 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated'
631670 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0'
631671 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft'
631671 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft'
631672 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft'
631673 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0'
631675 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch'
631751 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0'
631752 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch'
631871 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch'
631874 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch'
631879 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap'
631880 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated'
631881 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0'
631882 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft'
631884 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft'
631885 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft'
631885 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0'
631887 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch'
631893 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch'
631897 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch'
631981 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap'
631983 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated'
631984 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0'
631986 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft'
631988 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft'
631988 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft'
631989 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0'
631990 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch'
632037 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch'
632041 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch'
632117 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]''
632119 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective'
632120 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0''
632122 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0''
632123 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft'
632124 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch'
632227 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch'
632230 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0''
632232 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)''
632234 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight'
632235 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight'
632236 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight'
632237 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight'
632237 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch'
632244 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm'
632249 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0''
632251 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1''
632251 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch'
632328 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight'
632330 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight'
632331 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft'
632332 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0''
632332 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft'
632333 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch'
632420 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap'
632422 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated'
632423 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0'
632425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft'
632425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft'
632426 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft'
632427 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0'
632428 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch'
632518 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0'
632519 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch'
632580 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0''
632580 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft'
632581 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch'
632584 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch'
632587 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch'
632591 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch'
632689 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap'
632690 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated'
632691 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0'
632692 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch'
632699 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch'
632767 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch'
635954 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 149: 'cut '(int)s_0[v_y_0] = v_y_0''
635955 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)''
635960 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight'
635961 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight'
635962 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight'
635963 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight'
635965 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch'
635972 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm'
635973 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0''
635975 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0''
635976 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft'
635978 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch'
636060 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch'
636063 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight'
636064 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight'
636065 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft'
636065 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0''
636066 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft'
636067 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch'
636193 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap'
636194 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated'
636195 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0'
636196 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft'
636197 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft'
636197 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft'
636198 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0'
636199 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch'
636265 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0'
636266 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch'
636328 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch'
636332 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch'
636335 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap'
636336 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated'
636337 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0'
636338 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch'
636346 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch'
636414 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap'
636415 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated'
636416 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0'
636417 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch'
636480 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch'
636487 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0''
636488 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)''
636490 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight'
636491 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight'
636492 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight'
636492 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight'
636493 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch'
636502 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm'
636503 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0''
636504 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0''
636505 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft'
636506 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch'
636581 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))''
636583 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0''
636584 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0''
636585 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft'
636585 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch'
636663 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch'
636667 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight'
636668 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight'
636669 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft'
636669 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0''
636670 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft'
636670 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch'
636755 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap'
636756 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated'
636757 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0'
636758 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft'
636759 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft'
636760 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft'
636760 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0'
636761 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap'
636762 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated'
636763 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0'
636764 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft'
636765 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft'
636765 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft'
636766 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0'
636767 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch'
636842 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0'
636843 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch'
636849 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch'
636916 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch'
636985 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split'
636986 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap'
636987 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated'
636987 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0'
636988 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft'
636989 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft'
636989 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft'
636989 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0'
636990 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch'
637064 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch'
637069 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch'
637146 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap'
637147 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated'
637148 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0'
637149 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft'
637149 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft'
637150 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft'
637150 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0'
637151 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch'
637155 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0'
637156 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch'
637224 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch'
637228 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch'
637233 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch'
637318 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap'
637319 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated'
637320 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0'
637321 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft'
637321 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft'
637321 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft'
637321 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0'
637322 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch'
637369 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0'
637370 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap'
637370 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated'
637371 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0'
637372 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch'
637376 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch'
637381 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch'
637482 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch'
637559 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap'
637560 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated'
637560 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0'
637561 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch'
637708 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch'
637784 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0''
637784 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch'
640499 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm'
640504 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1''
640505 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0''
640506 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft'
640506 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch'
640605 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))''
640607 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1''
640608 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0''
640608 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft'
640609 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch'
640699 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch'
643336 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch'
646161 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)''
646166 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0''
646167 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0''
646168 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft'
646168 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch'
646267 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))''
646269 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0''
646270 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1''
646271 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...'
646272 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch'
647305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof
647305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.9ns
647306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
649748 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
649749 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1
650509 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1
650510 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns
650510 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
650516 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)''
650527 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x''
650529 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y''
650531 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft'
650531 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch'
650534 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft'
650536 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
650538 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1'
650540 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight'
650541 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch'
650548 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0''
650550 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight'
650550 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch'
650639 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight'
650640 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight'
650641 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0''
650641 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft'
650642 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch'
650701 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft'
650701 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange'
650703 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0''
650703 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft'
650704 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch'
650706 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
650707 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
650707 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange'
650708 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x''
650709 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft'
650709 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch'
650780 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
650781 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
650781 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange'
650782 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y''
650783 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft'
650784 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch'
650856 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
650856 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft'
650857 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0'
650857 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef'
650858 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0'
650859 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0'
650859 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0'
650859 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2'
650860 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft'
650860 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0'
650861 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0'
650861 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0'
650861 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0'
650862 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0'
650862 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0'
650863 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0'
650863 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0'
650864 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0'
650864 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch'
650866 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch'
650899 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0'
650900 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
650952 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0'
650953 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective'
650954 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0''
650955 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y''
650956 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft'
650956 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
651003 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch'
651005 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0'
651006 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective'
651007 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0''
651008 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x''
651009 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft'
651009 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch'
651058 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch'
651060 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch'
651063 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch'
651125 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch'
651182 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof
651182 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns
651183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
653548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
653548 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq
654346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq
654375 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.76ms