387 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key
411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.38ms
642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
659 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)
1576 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1578 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1582 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1583 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
2991 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
8393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.75s
8449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key
8477 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.5ns
8488 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof
8488 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.8ns
8492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
11333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
11335 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut
12278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut
12308 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.74ms
12325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof
12325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 420ns
12327 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
15048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s
15048 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight
15881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight
15895 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.41ms
15897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof
15897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.1ns
15898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
18548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s
18549 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1
19430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1
19446 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms
19452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof
19452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.1ns
19454 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
21997 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s
21998 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2
22865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2
22878 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.27ms
22881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof
22881 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.1ns
22882 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
25398 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s
25398 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos
26271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos
26344 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.21ms
26350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof
26350 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.9ns
26352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
28878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s
28878 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg
29722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg
29738 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms
29740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof
29740 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns
29741 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
32241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s
32241 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt
33083 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt
33086 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.8ns
33087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof
33088 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns
33088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
35584 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s
35585 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong
36397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong
36399 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 523ns
36400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof
36400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.6ns
36401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
38895 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s
38895 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort
39709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort
39711 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 551ns
39712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof
39713 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.4ns
39713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
42182 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
42182 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte
42991 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte
42993 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 513.3ns
42994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof
42994 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns
42995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
45449 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
45449 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar
46254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar
46258 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 872.11ns
46260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof
46260 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns
46261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
48718 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
48718 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1
49505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1
49543 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.21ms
49545 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof
49545 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.5ns
49546 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
52045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s
52045 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2
52848 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2
52881 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.64ms
52883 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof
52883 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.4ns
52884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
55339 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
55339 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists
56151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists
56311 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 150.57ms
56316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof
56316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.7ns
56317 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
58760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
58761 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one
59561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one
59567 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms
59569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof
59569 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 298ns
59570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
62033 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
62034 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one
62860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one
62863 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms
62865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof
62865 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns
62866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
65321 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
65323 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero
66112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero
66179 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.4ms
66183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof
66183 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.4ns
66184 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
68663 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s
68664 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1
69464 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1
69479 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.74ms
69481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof
69482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.8ns
69483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
71923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
71923 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2
72734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2
72749 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms
72751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof
72752 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 774.6ns
72756 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
75232 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s
75233 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1
76042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1
76057 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.74ms
76058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof
76058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns
76059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
78510 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
78511 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2
79313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2
79327 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.11ms
79329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof
79329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.4ns
79330 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
81794 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
81795 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1
82578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1
82605 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.52ms
82606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof
82606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns
82607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
85051 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
85052 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2
85850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2
85854 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms
85856 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof
85857 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.6ns
85858 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
88309 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
88310 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom
89111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom
89148 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.73ms
89150 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof
89150 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 105ns
89151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
91594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
91595 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus
92392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus
92443 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.54ms
92445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof
92445 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243ns
92446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
94890 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
94890 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom
95689 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom
95729 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.59ms
95732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof
95732 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.2ns
95733 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
98197 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
98197 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos
98977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos
98985 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms
98987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof
98987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.3ns
98988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
101451 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
101452 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg
102249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg
102262 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.35ms
102264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof
102264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.5ns
102265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
104702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
104703 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos
105500 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos
105511 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.57ms
105513 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof
105513 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.9ns
105514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
107953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
107954 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg
108748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg
108755 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.87ms
108757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof
108757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.6ns
108758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
111201 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
111202 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos
111996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos
112003 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms
112005 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof
112006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.8ns
112007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
114451 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
114451 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg
115229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg
115236 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms
115237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof
115237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns
115238 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
117723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s
117724 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero
118519 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero
118522 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms
118524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof
118525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.8ns
118525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
120959 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
120959 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum
121757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum
121767 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.71ms
121768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof
121768 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.8ns
121769 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
124198 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
124198 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom
124999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom
125051 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.82ms
125053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof
125054 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.8ns
125055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
127567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s
127567 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos
128361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos
128377 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms
128379 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof
128379 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.4ns
128380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
130808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
130809 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg
131604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg
131623 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.15ms
131624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof
131624 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns
131625 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
134056 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
134056 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos
134889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos
134907 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.98ms
134908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof
134908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns
134909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
137398 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s
137398 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg
138194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg
138210 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.48ms
138212 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof
138212 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns
138213 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
140639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
140639 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1
141433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1
141474 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.4ms
141476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof
141476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.2ns
141477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
143911 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
143911 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2
144704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2
144707 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms
144708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof
144708 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns
144709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
147133 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
147133 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero
147925 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero
147929 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms
147931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof
147931 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.9ns
147932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
150361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
150361 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom
151155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom
151162 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms
151163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof
151163 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns
151164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
153608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
153608 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos
154380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos
154388 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.92ms
154390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof
154390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns
154390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
156827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
156827 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg
157626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg
157645 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.02ms
157650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof
157650 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.6ns
157651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
160104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
160104 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero
160899 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero
160907 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms
160908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof
160908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns
160909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
163344 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
163345 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero
164154 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero
164157 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms
164160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof
164160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.9ns
164162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
166600 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
166601 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum
167392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum
167396 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms
167397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof
167397 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns
167398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
169825 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
169825 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom
170599 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom
170603 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms
170604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof
170604 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns
170605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
173046 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
173046 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1
173839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1
173907 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.9ms
173908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof
173908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.6ns
173909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
176356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
176356 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2
177152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2
177234 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.95ms
177236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof
177236 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.5ns
177237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
179655 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
179655 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem
180447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem
180450 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms
180451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof
180451 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns
180452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
182884 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
182885 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod
183676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod
183712 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.17ms
183715 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof
183721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.78ms
183721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
186158 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
186158 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible
186933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible
186960 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.89ms
186961 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof
186961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns
186962 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
189389 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
189389 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep
190181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep
190183 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 984.61ns
190184 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof
190184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns
190185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
192601 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
192601 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom
193389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom
193522 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 122.05ms
193525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof
193525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.2ns
193526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
195954 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
195955 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero
196760 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero
196770 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.17ms
196772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof
196772 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.4ns
196773 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
199217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
199217 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero
200010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero
200018 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.45ms
200019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof
200019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns
200020 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
202548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s
202548 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero
203392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero
203424 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.59ms
203427 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof
203427 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.7ns
203428 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
205972 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s
205972 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom
206774 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom
206795 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.82ms
206797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof
206798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.2ns
206799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
209224 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
209225 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty
210010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty
210014 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms
210015 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof
210015 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns
210016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
212420 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s
212421 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper
213209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper
213214 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms
213215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof
213215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.7ns
213216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
215632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
215632 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower
216425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower
216446 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.13ms
216450 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof
216450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.1ns
216451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
218896 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
218896 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds
219670 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds
219685 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.88ms
219687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof
219687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns
219687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
222118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
222118 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2
222941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2
222956 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms
222957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof
222957 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns
222958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
225412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
225412 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2
226201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2
226204 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms
226206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof
226206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns
226206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
228615 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
228615 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete
229402 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete
229406 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms
229407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof
229407 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 198ns
229408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
231839 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
231839 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2
232628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2
232633 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms
232634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof
232634 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns
232634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
235061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
235061 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete
235838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete
235841 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms
235842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof
235842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns
235842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
238259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
238259 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete
239046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete
239048 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.5ns
239049 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof
239049 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns
239049 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
241469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
241469 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2
242259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2
242262 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms
242263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof
242263 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns
242264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
244683 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
244683 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete
245473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete
245476 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms
245477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof
245477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns
245477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
247905 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
247905 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive
248694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive
248742 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.74ms
248744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof
248744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.9ns
248745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
251194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
251194 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound
251965 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound
251996 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.26ms
252009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof
252009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.5ns
252010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
254441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
254441 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound
255235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound
255263 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.19ms
255264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof
255264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns
255265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
257727 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
257727 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element
258519 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element
258557 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.22ms
258558 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof
258558 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns
258559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
260975 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
260975 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index
261764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index
261792 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.73ms
261793 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof
261793 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns
261794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
264233 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
264233 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index
265022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index
265069 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.96ms
265070 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof
265070 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns
265071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
267501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
267501 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index
268272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index
268296 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.48ms
268297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof
268297 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns
268298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
270723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
270723 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max
271515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max
271534 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.29ms
271535 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof
271535 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns
271536 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
273961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
273961 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2
274749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2
274773 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.75ms
274774 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof
274774 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns
274775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
277186 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
277186 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3
277979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3
277998 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms
277999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof
277999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns
278000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
280441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
280441 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4
281233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4
281262 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.08ms
281264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof
281264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns
281264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
283702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
283702 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max
284475 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max
284500 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.84ms
284501 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof
284501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns
284502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
286935 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
286936 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2
287727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2
287752 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ms
287753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof
287753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns
287754 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
290180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
290181 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3
290974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3
290998 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.16ms
290999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof
290999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns
291000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
293423 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
293423 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4
294215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4
294234 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.04ms
294235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof
294236 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns
294236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
296670 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
296670 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0
297461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0
297485 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.5ms
297486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof
297486 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns
297487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
299914 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
299914 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt
300684 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt
300709 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.48ms
300710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof
300710 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns
300711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
303144 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
303144 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete
303937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete
303946 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.45ms
303948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof
303948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.2ns
303949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
306385 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
306385 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive
307175 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive
307192 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.19ms
307193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof
307193 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns
307194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
309609 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
309609 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split
310400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split
310404 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms
310405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof
310405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns
310405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
312823 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
312823 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0
313611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0
313613 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.4ns
313614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof
313614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns
313615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
316050 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
316050 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1
316833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1
316835 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.1ns
316836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof
316836 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns
316837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
319264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
319264 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor
320055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor
320063 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms
320065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof
320065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns
320066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
322488 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
322488 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd
323279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd
323284 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms
323285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof
323286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns
323286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
325697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
325697 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono
326485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono
326496 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.08ms
326497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof
326497 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns
326498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
328929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
328930 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete
329727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete
329730 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms
329731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof
329731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns
329732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
332160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
332161 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight
332931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight
332933 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 491.2ns
332934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof
332934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns
332935 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
335348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
335348 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive
336135 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive
336140 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms
336141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof
336141 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns
336142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
338562 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
338562 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete
339353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete
339355 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.1ns
339356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof
339356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns
339357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
341845 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s
341845 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete
342618 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete
342620 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 525.9ns
342621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof
342621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns
342622 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
345048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
345048 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower
345839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower
345840 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.3ns
345841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof
345841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns
345842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
348265 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
348265 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper
349053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper
349056 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms
349057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof
349057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns
349058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
351476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
351477 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete
352269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete
352277 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ms
352279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof
352279 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns
352279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
354696 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
354697 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete
355486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete
355489 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms
355490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof
355491 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns
355491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
357908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
357908 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct
358696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct
358703 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms
358704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof
358704 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns
358704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
361120 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
361120 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete
361909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete
361913 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms
361914 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof
361914 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns
361914 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
364353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
364354 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity
365145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity
365161 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms
365162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof
365162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns
365163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
367579 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
367579 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete
368369 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete
368372 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms
368373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof
368373 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns
368374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
370790 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
370790 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity
371582 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity
371585 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms
371587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof
371587 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns
371587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
374006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
374006 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete
374796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete
374800 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms
374801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof
374801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns
374802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
377229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
377230 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive
378022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive
378037 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.32ms
378039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof
378039 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns
378040 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
380525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s
380525 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete
381361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete
381365 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 498.2ns
381367 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof
381367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.9ns
381368 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
383787 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
383787 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono
384559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono
384594 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.08ms
384596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof
384597 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.7ns
384597 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
387018 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
387018 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete
387808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete
387811 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms
387813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof
387813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns
387814 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
390240 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
390240 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess
391031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess
391052 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ms
391054 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof
391054 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.8ns
391055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
393480 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
393480 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2
394300 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2
394321 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.88ms
394323 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof
394323 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns
394324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
396773 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
396773 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow
397568 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow
397590 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.09ms
397591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof
397591 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns
397592 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
400017 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
400017 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete
400810 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete
400812 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.2ns
400813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof
400813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns
400814 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
403243 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
403243 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze
404034 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze
404040 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms
404041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof
404041 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns
404041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
406460 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
406460 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals
407252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals
407255 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms
407257 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof
407257 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.5ns
407258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
409683 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
409683 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1
410478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1
410481 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 690.6ns
410482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof
410482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.8ns
410482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
412905 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
412905 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2
413699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2
413701 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 745.6ns
413702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof
413702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns
413703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
416128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
416128 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1
416922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1
416924 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms
416925 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof
416925 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns
416926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
419342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
419342 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2
420135 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2
420137 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms
420138 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof
420138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns
420139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
422556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
422556 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges
423350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges
423359 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ms
423361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof
423361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns
423361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
425794 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
425794 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1
426591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1
426602 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.42ms
426604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof
426604 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns
426604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
429028 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
429028 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2
429821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2
429831 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms
429832 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof
429832 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns
429832 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
432249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
432249 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition
433046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition
433057 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.06ms
433058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof
433058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns
433059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
435480 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
435480 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue
436284 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue
436288 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms
436289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof
436289 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns
436290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
438716 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
438716 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny
439521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny
439528 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms
439530 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof
439530 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns
439531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
441950 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
441950 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast
442756 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast
442758 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.2ns
442759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof
442759 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns
442760 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
445174 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
445174 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton
445973 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton
445975 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms
445976 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof
445976 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns
445977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
448401 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
448401 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete
449200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete
449202 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 849.21ns
449203 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof
449203 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns
449204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
451628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
451629 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat
452427 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat
452437 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.09ms
452438 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof
452438 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns
452439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
454877 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
454877 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub
455681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub
455686 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms
455687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof
455688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.5ns
455688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
458108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
458108 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse
458906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse
458912 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms
458913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof
458913 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns
458914 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
461332 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
461332 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty
462131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty
462133 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.5ns
462134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof
462134 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns
462135 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
464550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
464550 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton
465345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton
465347 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.1ns
465348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof
465348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.1ns
465349 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
467765 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s
467765 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat
468563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat
468566 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms
468568 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof
468568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.2ns
468569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
471009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
471009 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub
471807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub
471809 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms
471810 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof
471810 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns
471811 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
474240 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
474240 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse
475041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse
475044 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms
475045 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof
475045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.5ns
475045 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
477456 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s
477456 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft
478254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft
478257 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms
478258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof
478258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns
478258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
480704 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
480704 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight
481509 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight
481514 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms
481515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof
481515 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns
481516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
483991 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
483991 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ
484804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ
484807 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms
484808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof
484808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns
484809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
487279 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
487279 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ
488089 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ
488099 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms
488100 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof
488100 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns
488101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
490551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
490551 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ
491358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ
491361 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.8ns
491362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof
491362 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns
491362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
493839 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s
493839 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ
494648 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ
494655 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.81ms
494657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof
494657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns
494658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
497124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
497125 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ
497936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ
497938 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 815.5ns
497939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof
497939 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns
497940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
500407 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
500407 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ
501211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ
501213 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 745.3ns
501214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof
501215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns
501215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
503690 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s
503690 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ
504497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ
504501 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms
504502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof
504502 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns
504503 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
506961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
506961 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ
507772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ
507775 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms
507777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof
507777 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.8ns
507778 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
510257 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s
510258 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ
511064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ
511067 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms
511068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof
511068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns
511069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
513532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
513532 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ
514337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ
514340 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms
514341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof
514342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns
514342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
516782 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
516782 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ
517607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ
517611 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms
517613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof
517613 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns
517613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
520066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
520066 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1
520872 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1
520886 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.36ms
520887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof
520887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns
520888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
523336 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
523337 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2
524160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2
524175 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.16ms
524177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof
524177 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns
524177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
526614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
526614 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty
527415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty
527425 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ms
527426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof
527426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns
527426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
529880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
529880 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete
530681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete
530691 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms
530693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof
530693 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns
530693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
533141 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
533141 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR
533944 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR
533969 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.51ms
533970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof
533970 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns
533971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
536439 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
536440 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL
537247 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL
537272 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.18ms
537273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof
537273 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns
537273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
539711 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
539711 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR
540513 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR
540536 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.77ms
540537 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof
540537 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns
540538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
542992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
542992 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL
543798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL
543812 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.93ms
543813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof
543813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns
543814 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
546275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
546275 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split
547081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split
547110 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.22ms
547111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof
547111 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns
547112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
549567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
549567 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper
550369 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper
550415 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.55ms
550417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof
550417 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.2ns
550418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
552889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
552889 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete
553697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete
553734 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.98ms
553736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof
553736 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 171ns
553736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
556213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s
556213 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower
557022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower
557063 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.77ms
557065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof
557065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns
557065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
559533 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
559533 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete
560363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete
560405 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.19ms
560406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof
560406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns
560407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
562856 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
562856 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three
563659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three
563775 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.45ms
563777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof
563777 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns
563777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
566231 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
566231 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty
567033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty
567040 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms
567041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof
567041 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns
567042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
569506 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
569506 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand
570311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand
570319 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.71ms
570320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof
570321 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 265ns
570321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
572785 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
572785 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper
573584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper
573589 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms
573591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof
573591 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns
573591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
576030 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
576030 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq
576853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq
576869 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.71ms
576870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof
576870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns
576871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
579301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
579301 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2
580101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2
580112 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.52ms
580113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof
580113 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns
580114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
582578 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
582578 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton
583380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton
583383 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms
583384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof
583384 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns
583385 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
585841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
585842 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst
586650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst
586666 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms
586668 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof
586668 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns
586668 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
589118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
589118 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond
589918 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond
589934 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.93ms
589935 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof
589935 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns
589935 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
592375 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
592375 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub
593180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub
593200 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.52ms
593201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof
593201 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns
593201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
595658 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
595658 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq
596462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq
596465 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 970ns
596466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof
596466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns
596467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
598928 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
598928 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq
599731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq
599734 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms
599736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof
599736 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns
599736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
602184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s
602184 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq
602984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq
602990 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms
602991 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof
602991 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns
602992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
605514 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s
605514 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv
606315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv
606323 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms
606324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof
606324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns
606325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
608753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
608754 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange
609563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange
609637 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.51ms
609639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof
609639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.1ns
609640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
612105 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
612105 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans
612908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans
612937 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.59ms
612938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof
612938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns
612939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
615370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s
615370 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl
616195 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl
616216 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.45ms
616217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof
616218 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns
616218 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
618676 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
618676 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit
619481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit
619483 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 267.7ns
619484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof
619484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns
619485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
621971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s
621971 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight
622775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight
622972 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 185.12ms
622974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof
622974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.1ns
622975 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
625452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s
625452 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap
626258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap
626307 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.36ms
626309 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof
626309 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns
626310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
628751 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
628751 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0
629580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0
629582 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 306.7ns
629583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof
629583 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns
629584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
632042 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
632042 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1
632848 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1
632849 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 323.5ns
632851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof
632851 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns
632851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
635311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
635312 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2
636119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2
636121 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.8ns
636122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof
636122 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns
636123 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
638580 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s
638580 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3
639384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3
639386 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 439.8ns
639387 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof
639387 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns
639388 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
641830 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
641830 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall
642654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall
642732 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.22ms
642736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof
642736 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.7ns
642737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
645206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
645206 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists
646015 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists
646063 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.38ms
646065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof
646065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns
646066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
648540 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s
648541 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2
649351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2
649353 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns
649382 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
649419 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight'
649436 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight'
649440 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop'
649445 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft''
649448 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft''
649449 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft''
649451 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
649454 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqNPermRange'
649456 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1'
649458 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft'
649459 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch'
649687 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft'
649689 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft'
649690 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1'
649691 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft'
649692 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch'
649831 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft'
649832 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft'
649833 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft'
649834 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2'
649836 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft'
649837 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch'
649985 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft'
649986 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
649987 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
649988 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2'
649989 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft'
649990 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch'
650103 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft'
650105 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
650106 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
650106 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1'
650107 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft'
650108 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch'
650115 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft'
650115 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
650116 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0'
650118 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1'
650119 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft'
650120 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch'
650127 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft'
650128 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft'
650129 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0'
650130 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv with='v_x_0''
650131 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft'
650131 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch'
650264 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv with='v_y_0''
650265 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft'
650266 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch'
650425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0''
650426 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)''
650429 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight'
650430 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight'
650431 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight'
650432 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight'
650432 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap'
650433 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
650436 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm'
650438 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1'
650439 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0''
650440 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft'
650441 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch'
650549 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
650553 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight'
650554 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight'
650555 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft'
650556 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0''
650556 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft'
650557 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch'
650682 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap'
650684 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated'
650685 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0'
650686 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft'
650687 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft'
650687 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft'
650688 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0'
650689 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch'
650781 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0'
650782 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch'
650902 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch'
650906 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch'
650912 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap'
650913 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated'
650914 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0'
650915 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft'
650915 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft'
650916 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft'
650916 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0'
650917 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch'
650926 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch'
650940 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch'
651035 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap'
651037 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated'
651037 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0'
651038 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft'
651039 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft'
651039 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft'
651040 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0'
651041 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch'
651101 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch'
651106 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch'
651213 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]''
651215 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective'
651217 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0''
651218 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0''
651219 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft'
651219 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch'
651337 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch'
651341 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0''
651342 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)''
651343 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight'
651344 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight'
651346 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight'
651346 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight'
651347 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch'
651356 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm'
651357 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0''
651358 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1''
651359 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch'
651472 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight'
651473 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight'
651474 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft'
651475 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0''
651475 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft'
651476 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch'
651578 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap'
651579 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated'
651580 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0'
651581 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft'
651582 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft'
651582 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft'
651583 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0'
651584 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch'
651664 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0'
651665 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch'
651735 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0''
651735 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft'
651736 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch'
651740 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch'
651744 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch'
651748 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch'
651859 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap'
651860 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated'
651861 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0'
651862 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch'
651872 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch'
651957 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch'
655359 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 149: 'cut '(int)s_0[v_y_0] = v_y_0''
655360 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)''
655366 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight'
655367 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight'
655368 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight'
655368 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight'
655369 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch'
655376 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm'
655378 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0''
655379 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0''
655380 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft'
655381 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch'
655470 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch'
655473 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight'
655476 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight'
655476 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft'
655477 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0''
655478 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft'
655478 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch'
655569 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap'
655570 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated'
655571 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0'
655572 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft'
655573 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft'
655573 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft'
655574 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0'
655575 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch'
655648 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0'
655650 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch'
655755 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch'
655759 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch'
655764 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap'
655765 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated'
655765 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0'
655766 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch'
655775 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch'
655851 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap'
655853 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated'
655853 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0'
655854 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch'
655924 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch'
655933 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0''
655934 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)''
655936 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight'
655937 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight'
655937 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight'
655938 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight'
655939 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch'
655949 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm'
655951 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0''
655952 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0''
655952 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft'
655953 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch'
656037 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))''
656039 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0''
656040 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0''
656041 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft'
656042 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch'
656129 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch'
656133 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight'
656134 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight'
656134 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft'
656134 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0''
656135 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft'
656136 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch'
656230 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap'
656231 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated'
656232 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0'
656233 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft'
656233 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft'
656233 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft'
656234 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0'
656235 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap'
656235 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated'
656236 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0'
656237 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft'
656237 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft'
656238 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft'
656238 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0'
656239 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch'
656324 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0'
656325 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch'
656330 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch'
656405 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch'
656482 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split'
656483 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap'
656484 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated'
656485 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0'
656485 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft'
656486 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft'
656486 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft'
656486 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0'
656487 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch'
656570 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch'
656576 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch'
656663 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap'
656664 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated'
656665 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0'
656666 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft'
656666 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft'
656666 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft'
656667 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0'
656667 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch'
656672 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0'
656673 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch'
656766 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch'
656771 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch'
656776 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch'
656873 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap'
656874 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated'
656875 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0'
656876 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft'
656876 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft'
656877 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft'
656877 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0'
656878 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch'
656931 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0'
656932 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap'
656933 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated'
656934 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0'
656935 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch'
656940 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch'
656945 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch'
657058 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch'
657178 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap'
657180 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated'
657181 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0'
657182 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch'
657343 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch'
657428 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0''
657429 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch'
660447 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm'
660452 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1''
660454 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0''
660455 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft'
660455 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch'
660564 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))''
660565 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1''
660567 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0''
660567 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft'
660568 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch'
660670 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch'
663732 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch'
667050 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)''
667056 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0''
667057 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0''
667058 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft'
667059 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch'
667202 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))''
667203 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0''
667212 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1''
667222 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)' ...'
667224 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch'
668465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof
668465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns
668466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
671136 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s
671137 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1
671929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1
671931 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns
671931 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
671937 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)''
671948 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x''
671950 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y''
671952 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft'
671953 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch'
671956 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft'
671958 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
671960 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1'
671963 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight'
671964 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch'
671971 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0''
671973 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight'
671974 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch'
672014 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight'
672015 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight'
672016 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0''
672016 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft'
672017 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch'
672079 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft'
672080 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange'
672081 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0''
672082 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft'
672082 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch'
672086 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
672086 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
672087 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange'
672088 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x''
672089 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft'
672089 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch'
672169 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
672170 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
672170 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange'
672171 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y''
672172 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft'
672173 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch'
672261 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
672262 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft'
672262 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0'
672263 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef'
672263 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0'
672264 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0'
672265 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0'
672265 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2'
672266 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft'
672266 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0'
672267 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0'
672267 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0'
672268 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0'
672268 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0'
672269 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0'
672269 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0'
672270 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0'
672271 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0'
672271 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch'
672274 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch'
672313 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0'
672314 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
672367 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0'
672368 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective'
672369 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0''
672371 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y''
672371 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft'
672372 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
672419 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch'
672422 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0'
672423 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective'
672424 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0''
672425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x''
672426 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft'
672427 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch'
672477 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch'
672479 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch'
672482 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch'
672537 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch'
672589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof
672589 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.1ns
672590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
675026 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
675026 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq
675850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq
675881 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.01ms