652 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key
674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.74ms
902 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
914 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)
1796 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1798 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1801 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1801 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
3167 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
8193 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.29s
8251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key
8308 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35ns
8320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof
8320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 499.8ns
8324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
11055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
11058 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut
11976 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut
11999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.72ms
12007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof
12008 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132ns
12009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
14630 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s
14631 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight
15464 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight
15478 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.48ms
15480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof
15480 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.1ns
15481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
18039 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s
18040 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1
18897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1
18913 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.04ms
18914 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof
18915 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.3ns
18916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
21319 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s
21319 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2
22119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2
22124 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms
22126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof
22126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.8ns
22127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
24568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s
24568 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos
25403 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos
25471 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.66ms
25474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof
25474 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.4ns
25475 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
27856 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
27857 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg
28636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg
28670 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.6ms
28674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof
28674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.3ns
28675 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
31062 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
31063 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt
31890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt
31894 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 551.4ns
31896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof
31896 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.6ns
31898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
34269 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
34269 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong
35062 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong
35064 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 496.4ns
35067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof
35067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.4ns
35068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
37416 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
37417 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort
38188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort
38191 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 561.3ns
38193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof
38194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.1ns
38195 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
40515 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
40516 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte
41306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte
41309 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 518ns
41311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof
41311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.9ns
41312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
43642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
43643 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar
44421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar
44425 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 984ns
44429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof
44429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.5ns
44430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
46801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
46801 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1
47545 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1
47584 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.96ms
47586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof
47586 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.4ns
47587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
49967 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
49968 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2
50732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2
50793 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.93ms
50800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof
50800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.7ns
50801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
53123 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
53123 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists
53888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists
54124 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 226.23ms
54127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof
54128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.4ns
54129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
56454 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
56454 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one
57215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one
57220 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms
57221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof
57221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns
57222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
59553 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
59554 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one
60319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one
60322 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms
60325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof
60325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.5ns
60327 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
62659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
62659 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero
63398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero
63434 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.78ms
63436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof
63436 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.7ns
63437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
65800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
65801 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1
66559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1
66574 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.24ms
66575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof
66576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.1ns
66576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
68883 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
68883 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2
69680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2
69695 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.54ms
69697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof
69699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.38ms
69703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
72030 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
72030 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1
72793 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1
72807 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms
72808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof
72808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns
72809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
75113 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
75113 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2
75872 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2
75886 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.16ms
75888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof
75888 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.6ns
75889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
78210 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
78211 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1
78947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1
78971 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.57ms
78972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof
78972 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.8ns
78973 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
81303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
81303 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2
82042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2
82045 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms
82046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof
82046 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns
82047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
84372 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
84373 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom
85139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom
85206 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.79ms
85208 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof
85208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.1ns
85209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
87537 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
87538 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus
88311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus
88368 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.04ms
88370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof
88370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.7ns
88372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
90684 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
90684 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom
91439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom
91479 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.99ms
91481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof
91481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns
91482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
93794 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
93795 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos
94556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos
94563 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.99ms
94564 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof
94565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns
94565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
96889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
96889 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg
97627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg
97639 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms
97640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof
97640 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns
97641 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
99951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
99951 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos
100705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos
100715 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ms
100716 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof
100716 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns
100717 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
103016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
103016 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg
103793 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg
103800 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms
103801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof
103801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns
103802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
106135 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
106135 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos
106895 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos
106903 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms
106906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof
106906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.5ns
106907 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
109210 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
109211 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg
109976 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg
109982 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms
109984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof
109984 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns
109985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
112300 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
112300 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero
113034 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero
113037 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms
113039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof
113039 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns
113039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
115367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
115367 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum
116101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum
116110 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.04ms
116113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof
116113 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns
116114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
118432 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
118433 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom
119191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom
119239 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.77ms
119240 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof
119240 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns
119241 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
121544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
121544 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos
122298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos
122313 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.22ms
122315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof
122315 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns
122316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
124607 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
124607 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg
125363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg
125378 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.97ms
125380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof
125380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns
125381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
127687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
127687 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos
128444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos
128460 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.18ms
128461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof
128461 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns
128462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
130781 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
130781 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg
131515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg
131530 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ms
131532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof
131532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns
131532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
133840 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
133841 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1
134594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1
134631 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.19ms
134633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof
134633 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns
134633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
136946 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
136947 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2
137704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2
137707 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms
137709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof
137709 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.2ns
137710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
140007 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
140007 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero
140762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero
140766 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms
140768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof
140768 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.6ns
140769 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
143065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
143065 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom
143822 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom
143829 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.37ms
143830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof
143831 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns
143831 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
146149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
146149 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos
146887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos
146899 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.49ms
146904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof
146904 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns
146905 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
149222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
149222 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg
149971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg
150011 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.84ms
150012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof
150012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns
150013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
152354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s
152354 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero
153105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero
153113 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms
153114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof
153114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns
153115 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
155404 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
155404 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero
156154 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero
156157 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms
156158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof
156158 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns
156159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
158450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
158451 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum
159211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum
159214 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms
159215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof
159215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns
159216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
161512 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
161512 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom
162263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom
162267 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms
162268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof
162268 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns
162269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
164568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
164568 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1
165299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1
165361 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.03ms
165362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof
165362 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns
165363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
167677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
167677 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2
168430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2
168498 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.18ms
168501 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof
168501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.7ns
168502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
170787 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
170787 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem
171538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem
171541 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms
171542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof
171542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns
171543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
173831 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
173831 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod
174585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod
174621 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.35ms
174625 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof
174627 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.14ms
174628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
176930 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
176930 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible
177685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible
177712 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.29ms
177713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof
177713 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns
177714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
180026 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
180026 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep
180761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep
180764 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms
180765 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof
180765 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns
180766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
183074 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
183074 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom
183827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom
183970 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 131.77ms
183972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof
183972 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns
183973 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
186276 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
186276 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero
187030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero
187040 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.88ms
187041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof
187041 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns
187042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
189339 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
189339 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero
190100 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero
190108 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.06ms
190109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof
190110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns
190110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
192407 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
192407 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero
193156 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero
193171 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms
193173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof
193173 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns
193173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
195489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
195490 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom
196222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom
196233 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.73ms
196235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof
196236 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns
196236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
198538 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
198538 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty
199271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty
199274 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms
199275 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof
199275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns
199276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
201587 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
201587 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper
202343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper
202347 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms
202348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof
202348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns
202349 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
204646 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
204646 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower
205400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower
205421 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.16ms
205423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof
205423 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.9ns
205424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
207714 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
207715 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds
208476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds
208493 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.07ms
208495 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof
208495 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns
208496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
210799 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
210799 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2
211562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2
211577 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.18ms
211578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof
211578 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns
211579 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
213891 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
213891 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2
214625 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2
214628 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms
214629 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof
214629 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns
214630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
216954 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
216954 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete
217709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete
217714 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms
217715 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof
217716 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.6ns
217717 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
220012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
220013 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2
220766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2
220771 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms
220772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof
220772 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns
220773 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
223076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
223076 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete
223831 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete
223834 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms
223835 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof
223835 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns
223836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
226132 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
226132 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete
226884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete
226886 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.1ns
226887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof
226887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns
226888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
229201 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
229201 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2
229934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2
229937 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms
229938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof
229939 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns
229939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
232263 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
232263 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete
232996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete
232999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 946.2ns
233000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof
233000 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns
233001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
235325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
235325 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive
236079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive
236126 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44ms
236128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof
236128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 191ns
236129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
238450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
238450 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound
239207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound
239255 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.34ms
239257 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof
239258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.3ns
239259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
241573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
241573 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound
242325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound
242363 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.96ms
242364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof
242364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns
242365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
244675 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
244675 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element
245442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element
245492 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.49ms
245493 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof
245493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns
245494 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
247822 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
247822 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index
248557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index
248588 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.52ms
248589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof
248590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns
248590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
250925 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
250925 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index
251687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index
251746 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.25ms
251748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof
251748 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns
251748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
254127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s
254127 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index
254881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index
254907 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.73ms
254908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof
254908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns
254909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
257206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
257206 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max
257964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max
257983 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ms
257985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof
257985 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns
257985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
260286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
260286 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2
261036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2
261060 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.88ms
261061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof
261061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns
261062 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
263367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
263367 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3
264097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3
264122 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.65ms
264123 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof
264124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns
264125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
266439 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
266439 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4
267187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4
267214 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.97ms
267215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof
267215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns
267216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
269507 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
269507 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max
270267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max
270292 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.3ms
270294 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof
270294 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns
270294 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
272589 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
272589 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2
273355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2
273379 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.94ms
273381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof
273381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns
273382 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
275670 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
275670 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3
276422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3
276446 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.17ms
276447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof
276447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns
276448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
278754 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
278754 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4
279486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4
279506 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.27ms
279507 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof
279508 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns
279508 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
281814 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
281814 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0
282571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0
282594 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms
282595 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof
282595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns
282596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
284894 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
284894 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt
285646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt
285670 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ms
285671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof
285671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns
285672 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
287958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
287959 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete
288711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete
288718 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms
288719 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof
288720 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns
288720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
291012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
291012 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive
291768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive
291785 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.28ms
291786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof
291786 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns
291787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
294097 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
294097 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split
294833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split
294836 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms
294838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof
294838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns
294838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
297187 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
297187 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0
297918 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0
297921 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.5ns
297922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof
297922 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns
297922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
300225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
300225 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1
300995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1
300998 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.8ns
300999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof
300999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns
301000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
303301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
303301 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor
304053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor
304059 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms
304061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof
304061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns
304061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
306342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
306342 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd
307097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd
307102 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms
307104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof
307104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns
307105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
309390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
309390 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono
310146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono
310157 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.14ms
310158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof
310158 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns
310159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
312461 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
312461 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete
313192 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete
313196 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms
313197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof
313197 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.6ns
313197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
315498 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
315499 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight
316249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight
316251 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 489.9ns
316252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof
316252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns
316253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
318534 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
318534 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive
319287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive
319293 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms
319294 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof
319294 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns
319294 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
321593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
321593 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete
322344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete
322346 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 639.4ns
322347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof
322349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.32ms
322350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
324635 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
324635 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete
325389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete
325391 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 520.7ns
325392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof
325392 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns
325393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
327705 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
327705 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower
328438 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower
328440 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 536.8ns
328441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof
328441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns
328442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
330754 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
330754 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper
331487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper
331491 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms
331492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof
331492 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns
331492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
333787 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
333787 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete
334538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete
334546 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.32ms
334547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof
334547 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns
334548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
336834 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
336834 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete
337589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete
337592 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms
337594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof
337594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns
337594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
339888 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
339888 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct
340644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct
340651 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms
340652 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof
340652 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns
340652 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
342942 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
342943 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete
343696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete
343700 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms
343701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof
343702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns
343702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
346015 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
346015 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity
346747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity
346762 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.26ms
346763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof
346763 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns
346764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
349077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
349077 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete
349837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete
349844 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms
349846 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof
349846 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.9ns
349846 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
352136 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
352136 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity
352888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity
352891 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms
352893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof
352893 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns
352893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
355180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
355180 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete
355932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete
355936 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms
355937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof
355937 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns
355938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
358222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
358222 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive
358977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive
358994 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms
358995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof
358995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns
358995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
361298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
361298 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete
362057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete
362061 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 462.3ns
362062 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof
362062 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns
362063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
364374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
364375 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono
365109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono
365145 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.3ms
365147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof
365147 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns
365147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
367461 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
367461 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete
368214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete
368217 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms
368219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof
368219 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns
368219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
370504 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
370504 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess
371256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess
371277 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.18ms
371278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof
371278 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns
371279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
373558 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
373558 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2
374308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2
374327 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms
374328 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof
374328 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns
374329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
376644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
376645 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow
377382 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow
377404 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.79ms
377406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof
377406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns
377406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
379743 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s
379744 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete
380501 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete
380504 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 519.1ns
380505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof
380505 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.1ns
380506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
382812 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
382812 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze
383570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze
383575 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms
383577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof
383577 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns
383577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
385884 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
385884 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals
386642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals
386645 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms
386646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof
386646 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns
386647 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
388977 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
388978 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1
389720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1
389723 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.7ns
389724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof
389724 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns
389725 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
392040 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
392040 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2
392796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2
392798 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.8ns
392799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof
392799 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns
392800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
395088 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
395088 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1
395844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1
395847 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms
395848 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof
395848 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns
395849 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
398127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
398127 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2
398886 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2
398888 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms
398889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof
398889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns
398890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
401195 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
401195 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges
401932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges
401942 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ms
401943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof
401943 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns
401944 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
404249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
404249 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1
405009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1
405023 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.59ms
405024 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof
405024 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns
405025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
407316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
407316 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2
408076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2
408088 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.33ms
408089 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof
408089 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns
408090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
410409 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
410409 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition
411152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition
411167 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.58ms
411169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof
411169 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns
411169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
413482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
413482 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue
414252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue
414258 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms
414261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof
414261 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.7ns
414262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
416577 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
416578 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny
417345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny
417350 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms
417351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof
417351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns
417352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
419680 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s
419681 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast
420422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast
420424 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 778.7ns
420425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof
420425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns
420426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
422723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
422723 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton
423489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton
423492 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms
423493 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof
423493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns
423494 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
425801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
425801 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete
426563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete
426565 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 881.5ns
426566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof
426566 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns
426567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
428861 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
428861 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat
429619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat
429629 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.18ms
429630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof
429630 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns
429631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
431925 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
431926 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub
432692 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub
432697 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms
432698 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof
432698 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns
432699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
434998 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
434999 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse
435739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse
435745 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms
435747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof
435747 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.3ns
435748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
438073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
438073 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty
438833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty
438835 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 638.4ns
438837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof
438837 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns
438837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
441114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
441114 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton
441874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton
441876 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 565.2ns
441877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof
441878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns
441878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
444175 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
444175 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat
444932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat
444935 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms
444936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof
444936 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns
444937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
447217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
447217 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub
447977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub
447979 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms
447980 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof
447980 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns
447981 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
450277 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
450277 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse
451035 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse
451038 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms
451039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof
451039 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.2ns
451040 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
453317 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
453317 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft
454074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft
454077 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms
454078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof
454078 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns
454078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
456377 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
456377 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight
457134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight
457140 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ms
457141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof
457141 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns
457141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
459422 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
459422 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ
460183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ
460186 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms
460187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof
460187 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns
460187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
462494 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
462494 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ
463254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ
463265 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms
463266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof
463266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns
463267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
465549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
465549 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ
466307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ
466310 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.9ns
466311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof
466311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158ns
466312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
468612 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
468612 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ
469370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ
469376 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms
469377 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof
469377 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns
469378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
471658 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
471658 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ
472416 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ
472418 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 871.5ns
472419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof
472419 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns
472419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
474715 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
474715 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ
475473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ
475475 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 751.9ns
475476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof
475476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns
475476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
477757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
477757 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ
478516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ
478520 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms
478521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof
478521 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns
478522 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
480823 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
480823 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ
481584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ
481587 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms
481588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof
481588 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns
481589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
483884 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
483884 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ
484623 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ
484626 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms
484628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof
484628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns
484628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
486924 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
486924 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ
487682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ
487686 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms
487687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof
487687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns
487688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
489996 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
489996 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ
490756 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ
490761 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms
490762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof
490762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns
490763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
493053 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
493053 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1
493811 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1
493825 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.98ms
493826 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof
493826 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns
493827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
496134 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
496134 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2
496891 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2
496906 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms
496907 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof
496907 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns
496908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
499202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
499203 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty
499942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty
499952 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.98ms
499953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof
499953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns
499954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
502247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
502247 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete
503005 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete
503019 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms
503020 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof
503020 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns
503021 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
505314 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
505314 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR
506072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR
506097 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.45ms
506098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof
506098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns
506099 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
508404 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
508404 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL
509176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL
509234 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.93ms
509235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof
509235 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns
509236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
511527 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
511527 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR
512286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR
512308 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.53ms
512309 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof
512310 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns
512310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
514616 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
514616 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL
515376 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL
515391 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ms
515393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof
515393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns
515393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
517689 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
517689 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split
518449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split
518477 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.79ms
518478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof
518478 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns
518479 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
520779 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
520780 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper
521521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper
521566 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.48ms
521567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof
521567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns
521568 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
523863 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
523863 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete
524621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete
524658 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.2ms
524659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof
524659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns
524660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
526960 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
526960 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower
527722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower
527762 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.69ms
527763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof
527763 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns
527764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
530067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
530067 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete
530830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete
530873 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.27ms
530874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof
530874 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns
530875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
533190 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
533190 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three
533953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three
534068 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.58ms
534069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof
534069 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns
534070 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
536382 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
536382 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty
537122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty
537129 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms
537131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof
537131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns
537131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
539422 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
539422 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand
540181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand
540189 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms
540196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof
540196 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns
540196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
542478 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s
542479 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper
543235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper
543241 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms
543242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof
543242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns
543243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
545534 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
545534 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq
546291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq
546308 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.89ms
546309 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof
546309 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns
546310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
548599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
548599 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2
549358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2
549369 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms
549370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof
549370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns
549370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
551666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
551666 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton
552424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton
552427 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms
552428 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof
552429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns
552429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
554722 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
554722 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst
555462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst
555479 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms
555480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof
555480 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns
555480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
557775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
557776 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond
558536 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond
558552 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.63ms
558553 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof
558553 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns
558554 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
560850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
560850 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub
561647 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub
561666 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.05ms
561668 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof
561668 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.1ns
561669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
564056 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s
564056 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq
564829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq
564832 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms
564833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof
564833 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns
564833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
567120 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
567120 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq
567878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq
567881 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms
567882 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof
567882 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns
567883 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
570179 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
570179 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq
570940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq
570946 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms
570947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof
570947 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns
570948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
573256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
573256 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv
574016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv
574022 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms
574023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof
574024 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns
574024 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
576316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s
576316 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange
577076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange
577143 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.27ms
577145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof
577145 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns
577145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
579506 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s
579506 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans
580266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans
580291 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.97ms
580292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof
580292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns
580293 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
582594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
582594 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl
583358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl
583380 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.19ms
583381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof
583381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns
583382 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
585683 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
585683 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit
586449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit
586451 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 296.3ns
586452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof
586453 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns
586453 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
588754 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
588754 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight
589513 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight
589702 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 177.32ms
589703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof
589703 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107ns
589704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
592015 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
592015 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap
592801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap
592849 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.86ms
592850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof
592850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns
592851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
595223 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
595223 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0
595985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0
595987 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 337.2ns
595988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof
595988 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns
595989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
598295 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
598295 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1
599055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1
599057 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 315.9ns
599058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof
599058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns
599059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
601354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s
601354 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2
602121 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2
602123 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 324.4ns
602124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof
602124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns
602125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
604441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s
604441 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3
605206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3
605208 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 432.6ns
605209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof
605209 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns
605210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
607552 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s
607552 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall
608315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall
608421 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.79ms
608423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof
608423 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.3ns
608424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
610773 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s
610773 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists
611542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists
611593 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.59ms
611594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof
611594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns
611599 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
613908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s
613908 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2
614668 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2
614669 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ns
614692 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
614725 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight'
614741 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight'
614745 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop'
614750 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft''
614753 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft''
614754 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft''
614756 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
614758 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqNPermRange'
614760 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1'
614762 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft'
614763 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch'
614947 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft'
614948 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft'
614949 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1'
614950 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft'
614951 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch'
615050 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft'
615052 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft'
615052 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft'
615054 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2'
615055 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft'
615056 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch'
615212 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft'
615214 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
615215 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
615215 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2'
615216 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft'
615217 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch'
615325 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft'
615326 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
615327 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
615328 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1'
615329 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft'
615330 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch'
615336 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft'
615337 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
615337 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0'
615339 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1'
615340 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft'
615341 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch'
615347 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft'
615348 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft'
615348 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0'
615349 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv with='v_x_0''
615350 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft'
615351 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch'
615477 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv with='v_y_0''
615478 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft'
615479 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch'
615587 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0''
615589 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)''
615592 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight'
615593 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight'
615594 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight'
615595 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight'
615595 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap'
615596 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
615604 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm'
615605 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1'
615606 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0''
615607 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft'
615608 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch'
615707 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
615711 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight'
615712 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight'
615713 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft'
615714 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0''
615715 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft'
615715 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch'
615821 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap'
615823 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated'
615824 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0'
615825 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft'
615826 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft'
615827 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft'
615827 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0'
615828 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch'
615909 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0'
615910 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch'
616025 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch'
616029 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch'
616033 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap'
616034 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated'
616035 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0'
616036 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft'
616037 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft'
616037 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft'
616038 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0'
616039 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch'
616046 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch'
616050 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch'
616139 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap'
616140 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated'
616141 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0'
616142 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft'
616143 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft'
616143 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft'
616143 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0'
616144 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch'
616189 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch'
616194 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch'
616273 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]''
616275 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective'
616277 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0''
616278 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0''
616279 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft'
616280 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch'
616396 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch'
616400 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0''
616401 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)''
616403 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight'
616404 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight'
616404 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight'
616405 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight'
616406 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch'
616414 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm'
616415 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0''
616417 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1''
616417 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch'
616542 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight'
616544 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight'
616545 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft'
616545 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0''
616546 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft'
616547 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch'
616640 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap'
616641 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated'
616642 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0'
616643 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft'
616644 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft'
616644 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft'
616645 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0'
616646 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch'
616722 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0'
616724 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch'
616794 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0''
616795 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft'
616795 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch'
616799 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch'
616803 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch'
616807 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch'
616920 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap'
616921 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated'
616922 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0'
616923 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch'
616932 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch'
617013 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch'
620419 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 149: 'cut '(int)s_0[v_y_0] = v_y_0''
620420 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)''
620426 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight'
620427 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight'
620433 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight'
620434 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight'
620435 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch'
620442 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm'
620443 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0''
620445 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0''
620445 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft'
620446 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch'
620572 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch'
620576 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight'
620577 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight'
620577 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft'
620578 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0''
620579 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft'
620579 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch'
620667 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap'
620668 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated'
620669 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0'
620670 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft'
620671 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft'
620671 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft'
620672 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0'
620673 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch'
620745 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0'
620746 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch'
620818 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch'
620822 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch'
620826 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap'
620827 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated'
620828 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0'
620829 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch'
620838 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch'
620917 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap'
620918 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated'
620919 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0'
620919 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch'
620992 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch'
621001 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0''
621003 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)''
621005 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight'
621006 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight'
621006 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight'
621007 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight'
621007 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch'
621018 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm'
621019 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0''
621020 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0''
621021 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft'
621022 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch'
621110 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))''
621112 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0''
621113 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0''
621114 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft'
621115 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch'
621206 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch'
621210 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight'
621211 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight'
621212 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft'
621213 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0''
621213 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft'
621214 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch'
621312 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap'
621314 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated'
621315 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0'
621316 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft'
621316 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft'
621317 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft'
621317 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0'
621319 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap'
621320 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated'
621320 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0'
621321 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft'
621322 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft'
621322 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft'
621323 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0'
621323 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch'
621407 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0'
621408 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch'
621414 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch'
621488 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch'
621565 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split'
621567 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap'
621568 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated'
621569 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0'
621569 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft'
621570 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft'
621570 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft'
621571 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0'
621572 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch'
621654 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch'
621660 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch'
621747 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap'
621748 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated'
621749 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0'
621750 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft'
621750 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft'
621751 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft'
621751 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0'
621752 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch'
621757 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0'
621758 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch'
621834 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch'
621839 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch'
621845 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch'
621940 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap'
621941 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated'
621942 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0'
621943 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft'
621944 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft'
621944 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft'
621944 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0'
621945 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch'
621998 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0'
622000 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap'
622000 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated'
622001 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0'
622002 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch'
622007 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch'
622012 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch'
622123 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch'
622246 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap'
622247 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated'
622248 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0'
622249 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch'
622416 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch'
622500 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0''
622501 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch'
625457 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm'
625463 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1''
625464 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0''
625465 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft'
625466 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch'
625618 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))''
625620 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1''
625621 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0''
625622 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft'
625623 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch'
625722 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch'
628595 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch'
631669 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)''
631674 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0''
631675 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0''
631675 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft'
631676 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch'
631785 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))''
631787 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0''
631788 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1''
631788 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)' ...'
631790 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch'
632915 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof
632916 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns
632916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
635288 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
635288 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1
636072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1
636073 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns
636074 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
636079 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)''
636091 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x''
636093 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y''
636095 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft'
636095 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch'
636099 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft'
636101 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
636103 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1'
636106 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight'
636106 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch'
636114 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0''
636115 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight'
636116 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch'
636160 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight'
636161 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight'
636161 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0''
636162 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft'
636162 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch'
636230 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft'
636231 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange'
636232 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0''
636233 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft'
636233 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch'
636236 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
636237 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
636237 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange'
636238 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x''
636239 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft'
636239 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch'
636327 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
636328 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
636328 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange'
636329 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y''
636330 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft'
636330 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch'
636421 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
636422 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft'
636422 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0'
636422 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef'
636423 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0'
636424 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0'
636424 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0'
636424 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2'
636425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft'
636425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0'
636425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0'
636426 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0'
636426 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0'
636427 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0'
636427 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0'
636427 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0'
636428 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0'
636428 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0'
636477 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch'
636480 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch'
636518 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0'
636519 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
636580 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0'
636581 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective'
636582 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0''
636583 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y''
636585 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft'
636585 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
636630 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch'
636632 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0'
636634 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective'
636635 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0''
636636 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x''
636637 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft'
636637 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch'
636680 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch'
636683 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch'
636685 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch'
636731 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch'
636780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof
636780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.5ns
636781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
639154 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s
639154 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq
639959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq
639989 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.8ms