545 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key
570 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.4ms
819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
835 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)
2246 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
2248 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
2252 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
2253 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
3875 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
10412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 9.59s
10482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key
10521 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.9ns
10534 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof
10535 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.02ns
10540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
13861 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s
13864 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut
14996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut
15025 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.79ms
15040 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof
15040 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.22ns
15042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
18136 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s
18136 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight
19381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight
19415 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.08ms
19424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof
19424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.31ns
19431 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
22658 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s
22658 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1
23681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1
23689 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms
23699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof
23700 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 556.24ns
23704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
26707 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
26708 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2
27777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2
27792 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms
27800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof
27801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.6ms
27805 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
30924 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s
30925 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos
31929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos
31976 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.06ms
31980 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof
31981 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 779.15ns
31982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
35144 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s
35145 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg
36223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg
36263 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.65ms
36265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof
36265 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.01ns
36266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
39452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s
39452 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt
40554 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt
40560 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms
40563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof
40564 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 520.13ns
40566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
43849 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s
43850 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong
44943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong
44947 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.05ns
44951 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof
44952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.23ns
44953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
48109 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s
48109 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort
49137 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort
49140 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.75ns
49144 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof
49144 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 588.64ns
49146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
52441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s
52443 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte
53510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte
53515 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 766.65ns
53522 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof
53522 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 487.63ns
53524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
56559 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
56560 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar
57508 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar
57511 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.94ns
57515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof
57516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 420.23ns
57517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
60379 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
60380 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1
61411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1
61513 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.83ms
61515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof
61515 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.11ns
61516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
64406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s
64406 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2
65321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2
65356 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.13ms
65359 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof
65359 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.01ns
65360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
68231 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
68231 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists
69146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists
69378 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 224.25ms
69383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof
69383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.82ns
69384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
72416 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
72417 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one
73419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one
73426 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms
73431 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof
73432 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 583.44ns
73434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
76379 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
76380 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one
77294 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one
77297 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms
77301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof
77302 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.62ns
77303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
80196 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s
80196 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero
81109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero
81166 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.68ms
81170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof
81170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.41ns
81171 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
84240 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s
84240 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1
85243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1
85263 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.18ms
85266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof
85266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.03ns
85267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
88237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
88237 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2
89214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2
89230 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.11ms
89232 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof
89233 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.61ns
89234 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
92122 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s
92122 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1
93117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1
93135 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.24ms
93138 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof
93139 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.83ns
93140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
95965 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
95967 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2
96960 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2
96983 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.85ms
96987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof
96988 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 661.94ns
96990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
100090 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s
100091 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1
101117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1
101164 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.17ms
101168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof
101168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.13ns
101170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
104044 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
104044 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2
104980 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2
104983 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms
104985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof
104985 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.71ns
104986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
107896 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
107897 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom
108910 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom
108957 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.83ms
108960 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof
108961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 577.54ns
108962 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
111937 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
111937 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus
112877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus
112941 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.11ms
112945 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof
112945 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.33ns
112947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
115770 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
115771 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom
116736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom
116841 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.38ms
116846 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof
116848 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.46ms
116850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
119953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s
119956 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos
120954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos
120966 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ms
120968 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof
120968 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.42ns
120972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
123857 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
123857 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg
124866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg
124889 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.6ms
124895 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof
124897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.95ms
124900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
127838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
127838 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos
128800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos
128813 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.98ms
128815 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof
128815 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.91ns
128816 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
131778 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
131779 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg
132712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg
132722 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.07ms
132724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof
132724 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.52ns
132725 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
135743 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
135744 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos
136763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos
136775 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ms
136779 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof
136780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.52ns
136781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
139763 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
139763 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg
140667 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg
140676 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms
140677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof
140677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.11ns
140678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
143556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
143556 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero
144480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero
144484 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms
144487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof
144487 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.02ns
144488 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
147408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s
147409 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum
148392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum
148408 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms
148413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof
148414 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.93ns
148415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
151275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
151275 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom
152181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom
152249 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.73ms
152252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof
152252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.32ns
152254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
155098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
155099 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos
156033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos
156056 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.54ms
156058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof
156058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.21ns
156059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
159059 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
159059 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg
160023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg
160064 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.01ms
160067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof
160068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.63ns
160069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
163037 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
163037 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos
163966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos
163986 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.93ms
163987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof
163988 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.31ns
163988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
166801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
166801 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg
167808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg
167834 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.95ms
167835 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof
167835 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.41ns
167836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
170663 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
170663 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1
171609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1
171654 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.31ms
171656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof
171656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.81ns
171657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
174451 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
174451 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2
175411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2
175414 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms
175415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof
175415 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.91ns
175416 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
178280 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
178281 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero
179208 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero
179213 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms
179215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof
179215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.21ns
179216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
182006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
182007 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom
182987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom
182998 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.41ms
183004 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof
183005 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.63ns
183006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
185972 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
185972 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos
186896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos
186906 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ms
186907 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof
186907 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.61ns
186908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
189683 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
189683 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg
190616 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg
190637 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.83ms
190638 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof
190638 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.11ns
190639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
193542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
193542 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero
194551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero
194560 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.57ms
194562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof
194562 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.11ns
194563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
197466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
197466 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero
198477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero
198481 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms
198484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof
198484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.82ns
198485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
201277 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
201278 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum
202204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum
202208 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms
202210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof
202210 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.21ns
202210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
204995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
204995 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom
205922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom
205926 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms
205928 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof
205928 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.51ns
205929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
208808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
208809 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1
209746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1
209824 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.21ms
209826 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof
209826 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.11ns
209827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
212646 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
212647 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2
213546 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2
213642 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.12ms
213644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof
213644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.61ns
213645 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
216573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
216573 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem
217491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem
217500 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms
217503 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof
217503 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.81ns
217505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
220408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
220409 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod
221311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod
221351 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.33ms
221353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof
221354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.32ns
221355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
224193 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
224193 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible
225091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible
225125 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.46ms
225127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof
225127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.91ns
225128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
227990 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
227990 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep
229033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep
229037 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms
229040 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof
229040 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.33ns
229042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
232051 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s
232051 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom
232997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom
233162 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 152.8ms
233165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof
233165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.52ns
233166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
236064 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
236064 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero
237100 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero
237115 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms
237117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof
237117 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns
237118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
239935 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
239935 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero
240865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero
240874 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.49ms
240875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof
240875 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.01ns
240876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
243725 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
243725 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero
244649 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero
244668 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.82ms
244669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof
244670 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.61ns
244670 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
247467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
247467 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom
248389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom
248403 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.58ms
248405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof
248405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.81ns
248406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
251184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
251185 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty
252107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty
252111 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms
252113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof
252113 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.71ns
252114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
254908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
254909 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper
255835 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper
255840 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms
255842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof
255842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.81ns
255843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
258674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
258674 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower
259619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower
259648 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.97ms
259650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof
259650 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.61ns
259651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
262473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
262473 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds
263405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds
263424 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.25ms
263426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof
263426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns
263427 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
266306 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
266306 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2
267285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2
267303 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.69ms
267305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof
267305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.01ns
267305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
270104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
270105 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2
271028 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2
271032 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms
271034 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof
271034 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns
271035 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
273807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
273807 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete
274819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete
274825 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms
274826 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof
274826 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.11ns
274827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
277808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
277808 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2
278746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2
278752 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms
278753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof
278753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.21ns
278754 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
281619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
281619 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete
282517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete
282520 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms
282522 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof
282522 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.91ns
282523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
285346 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
285346 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete
286244 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete
286247 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 790.75ns
286248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof
286249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.91ns
286249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
289070 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
289070 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2
289970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2
289974 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms
289976 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof
289976 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.61ns
289977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
292846 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
292846 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete
293741 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete
293744 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms
293745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof
293745 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns
293746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
296540 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
296540 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive
297448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive
297532 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.47ms
297535 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof
297536 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.42ns
297537 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
300440 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
300440 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound
301350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound
301406 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.97ms
301407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof
301408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.21ns
301409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
304208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
304208 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound
305136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound
305183 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.28ms
305184 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof
305184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.91ns
305185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
308009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
308009 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element
308997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element
309075 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.82ms
309077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof
309077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.71ns
309078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
311942 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
311942 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index
312877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index
312915 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.44ms
312916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof
312916 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.81ns
312917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
315982 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
315982 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index
316908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index
316966 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.44ms
316968 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof
316968 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.31ns
316969 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
319765 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
319765 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index
320693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index
320725 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.19ms
320726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof
320727 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.51ns
320727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
323656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
323656 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max
324582 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max
324605 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms
324607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof
324607 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.81ns
324608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
327387 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
327387 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2
328352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2
328384 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.05ms
328385 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof
328386 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.31ns
328386 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
331318 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
331318 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3
332285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3
332309 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.65ms
332311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof
332311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.01ns
332312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
335118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
335119 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4
336055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4
336088 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.85ms
336091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof
336091 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.82ns
336092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
338880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
338880 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max
339825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max
339854 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.44ms
339855 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof
339855 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.11ns
339865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
342828 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
342829 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2
343817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2
343849 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.93ms
343851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof
343851 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.71ns
343852 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
346684 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
346684 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3
347628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3
347657 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.71ms
347659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof
347659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.51ns
347660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
350513 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
350514 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4
351413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4
351437 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.14ms
351439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof
351439 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.51ns
351440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
354285 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
354285 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0
355204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0
355231 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.07ms
355233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof
355233 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns
355234 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
358206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
358206 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt
359114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt
359142 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.12ms
359144 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof
359144 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.31ns
359145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
362096 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
362096 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete
363030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete
363042 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms
363043 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof
363043 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.81ns
363044 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
366016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
366016 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive
366942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive
366971 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.09ms
366972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof
366973 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.01ns
366977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
369800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
369800 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split
370733 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split
370738 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms
370739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof
370739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns
370740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
373566 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
373566 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0
374508 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0
374510 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.14ns
374512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof
374512 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns
374513 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
377297 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
377297 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1
378227 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1
378229 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 857.55ns
378231 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof
378231 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.11ns
378232 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
381048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
381048 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor
381977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor
381990 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms
381993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof
381993 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.21ns
381994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
384842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
384842 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd
385840 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd
385848 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms
385850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof
385858 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.18ms
385860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
388695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
388696 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono
389625 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono
389639 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.51ms
389640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof
389641 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.41ns
389641 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
392488 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
392488 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete
393424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete
393428 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms
393429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof
393429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns
393430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
396223 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
396224 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight
397155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight
397157 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 603.14ns
397158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof
397159 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.91ns
397159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
400042 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
400042 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive
400968 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive
400975 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms
400976 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof
400976 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.11ns
400977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
403769 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
403769 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete
404695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete
404698 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720.35ns
404699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof
404699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns
404700 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
407516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
407516 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete
408443 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete
408446 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665.24ns
408447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof
408447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns
408448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
411367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s
411367 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower
412296 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower
412298 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.64ns
412300 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof
412300 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns
412300 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
415184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
415184 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper
416124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper
416128 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms
416130 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof
416130 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.91ns
416130 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
418921 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
418922 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete
419886 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete
419896 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.16ms
419898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof
419898 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns
419899 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
422703 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
422703 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete
423630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete
423634 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms
423636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof
423636 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.31ns
423638 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
426451 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
426451 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct
427352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct
427360 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms
427362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof
427362 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.91ns
427363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
430179 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
430179 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete
431131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete
431138 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.07ms
431143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof
431144 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 634.44ns
431145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
434083 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
434083 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity
435076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity
435095 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.89ms
435096 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof
435096 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns
435097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
438025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
438025 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete
438989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete
438994 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms
438995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof
438995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns
438996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
441931 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
441931 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity
442884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity
442888 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms
442889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof
442889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.51ns
442890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
445704 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
445704 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete
446603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete
446607 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms
446609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof
446609 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns
446610 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
449477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
449477 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive
450405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive
450425 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.24ms
450427 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof
450427 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns
450427 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
453262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
453262 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete
454204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete
454213 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.44ns
454216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof
454216 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.72ns
454217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
457058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
457058 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono
457981 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono
458028 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.57ms
458029 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof
458030 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.11ns
458030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
460813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
460813 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete
461744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete
461748 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms
461749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof
461749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns
461750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
464580 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
464581 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess
465512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess
465538 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.31ms
465539 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof
465539 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.41ns
465540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
468332 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
468332 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2
469341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2
469369 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.59ms
469371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof
469371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.11ns
469372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
472375 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
472375 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow
473303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow
473331 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.07ms
473333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof
473333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.41ns
473334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
476151 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
476151 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete
477112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete
477116 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.25ns
477118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof
477118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.62ns
477119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
479941 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
479941 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze
480915 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze
480922 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.07ms
480924 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof
480924 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns
480925 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
483782 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
483782 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals
484715 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals
484718 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms
484720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof
484720 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns
484721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
487493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
487494 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1
488424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1
488427 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 944.56ns
488429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof
488429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns
488429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
491213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
491213 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2
492247 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2
492250 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms
492252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof
492252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns
492253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
495093 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
495093 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1
496031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1
496035 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms
496037 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof
496037 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.81ns
496037 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
498904 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
498904 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2
499814 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2
499818 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms
499820 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof
499820 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.11ns
499821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
502837 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
502837 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges
503741 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges
503753 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.76ms
503755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof
503755 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.11ns
503755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
506560 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
506561 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1
507477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1
507491 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.72ms
507493 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof
507493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.61ns
507494 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
510367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
510367 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2
511299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2
511311 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.07ms
511312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof
511312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns
511313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
514117 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
514117 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition
515071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition
515096 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.23ms
515099 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof
515099 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.81ns
515100 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
517927 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
517927 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue
518906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue
518912 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms
518914 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof
518914 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.71ns
518915 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
522022 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s
522022 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny
523087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny
523095 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms
523096 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof
523096 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.31ns
523097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
526258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s
526259 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast
527295 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast
527298 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms
527300 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof
527300 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.61ns
527301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
530239 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
530240 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton
531175 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton
531179 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms
531181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof
531181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns
531181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
533978 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
533978 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete
534886 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete
534889 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms
534890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof
534890 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns
534891 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
537795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
537796 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat
538826 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat
538840 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.78ms
538842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof
538842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns
538843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
541690 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
541690 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub
542671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub
542676 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms
542677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof
542677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.81ns
542678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
545501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
545501 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse
546439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse
546447 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms
546448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof
546448 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.11ns
546449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
549227 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
549228 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty
550167 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty
550169 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 901.56ns
550171 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof
550171 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns
550172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
553138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
553138 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton
554093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton
554095 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 730.15ns
554097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof
554097 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.11ns
554098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
557003 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
557003 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat
557922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat
557926 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms
557928 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof
557928 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.31ns
557929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
560782 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
560782 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub
561723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub
561726 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms
561728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof
561728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns
561728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
564663 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
564664 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse
565634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse
565638 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms
565639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof
565639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns
565640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
568412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s
568412 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft
569385 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft
569389 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms
569390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof
569390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns
569391 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
572222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
572222 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight
573133 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight
573141 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms
573142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof
573143 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns
573143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
575973 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s
575973 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ
576927 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ
576931 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms
576932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof
576932 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns
576933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
579872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
579872 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ
580850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ
580863 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ms
580864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof
580865 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.31ns
580865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
583748 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
583748 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ
584733 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ
584736 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 797.65ns
584737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof
584737 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns
584738 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
587810 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s
587810 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ
588780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ
588790 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.16ms
588791 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof
588791 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns
588792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
591725 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
591725 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ
592690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ
592693 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms
592694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof
592694 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns
592695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
595607 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
595607 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ
596552 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ
596555 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 869.56ns
596556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof
596556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns
596557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
599445 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s
599445 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ
600357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ
600363 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms
600364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof
600364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns
600365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
603222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
603222 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ
604159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ
604162 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms
604164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof
604164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns
604165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
606941 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
606941 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ
607878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ
607881 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms
607883 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof
607883 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns
607884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
610687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
610687 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ
611599 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ
611603 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms
611604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof
611604 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns
611605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
614533 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
614534 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ
615498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ
615504 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms
615505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof
615506 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.41ns
615506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
618295 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
618295 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1
619233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1
619250 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.51ms
619251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof
619252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.31ns
619252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
622128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
622128 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2
623042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2
623060 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms
623062 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof
623062 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.21ns
623063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
625883 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
625884 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty
626832 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty
626848 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.11ms
626850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof
626850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.81ns
626851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
629911 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
629911 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete
630852 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete
630865 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.23ms
630866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof
630866 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns
630867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
633710 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
633710 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR
634646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR
634676 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.2ms
634677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof
634678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns
634678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
637482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
637482 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL
638420 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL
638449 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.93ms
638451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof
638451 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.31ns
638452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
641444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
641444 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR
642418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR
642445 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.12ms
642447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof
642447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns
642448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
645246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
645246 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL
646285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL
646309 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.88ms
646311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof
646311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.01ns
646312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
649183 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
649183 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split
650093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split
650129 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.12ms
650130 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof
650130 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.91ns
650131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
653072 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
653072 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper
654014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper
654069 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.49ms
654070 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof
654071 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns
654072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
656983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
656983 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete
657898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete
657944 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.52ms
657946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof
657946 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.51ns
657947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
660907 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
660908 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower
661932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower
661985 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.03ms
661986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof
661986 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.91ns
661987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
665189 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s
665189 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete
666202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete
666257 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.59ms
666258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof
666259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.21ns
666260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
669321 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
669321 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three
670318 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three
670473 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 146.71ms
670475 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof
670475 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.21ns
670476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
673435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
673435 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty
674433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty
674442 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.86ms
674443 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof
674443 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns
674444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
677444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
677444 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand
678538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand
678547 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms
678548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof
678549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.41ns
678549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
681387 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
681387 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper
682335 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper
682341 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms
682342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof
682342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.31ns
682343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
685182 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
685183 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq
686120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq
686141 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.4ms
686142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof
686142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.31ns
686143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
688934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
688934 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2
689884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2
689897 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.61ms
689898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof
689899 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.31ns
689899 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
692768 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
692768 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton
693704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton
693708 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms
693709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof
693710 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns
693710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
696551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
696552 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst
697486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst
697508 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.89ms
697510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof
697511 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.62ns
697512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
700373 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s
700373 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond
701286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond
701305 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms
701306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof
701306 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.81ns
701307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
704131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
704131 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub
705066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub
705089 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.35ms
705090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof
705090 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.61ns
705091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
708066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
708066 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq
709072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq
709076 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms
709077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof
709077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.61ns
709078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
711877 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
711878 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq
712858 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq
712862 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms
712864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof
712864 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns
712865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
715687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
715687 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq
716651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq
716658 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.58ms
716660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof
716660 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.71ns
716661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
719697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
719697 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv
720685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv
720692 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms
720694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof
720694 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns
720695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
723516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
723516 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange
724500 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange
724588 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.44ms
724590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof
724590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.41ns
724591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
727533 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
727533 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans
728470 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans
728501 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.49ms
728502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof
728503 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns
728503 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
731311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
731312 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl
732287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl
732314 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.55ms
732315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof
732316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.61ns
732316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
735134 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
735134 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit
736069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit
736071 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 334.52ns
736073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof
736073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns
736074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
738882 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
738882 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight
739819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight
740054 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.58ms
740056 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof
740057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.62ns
740058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
742899 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
742899 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap
743873 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap
743934 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.31ms
743935 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof
743935 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.61ns
743936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
746760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s
746760 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0
747764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0
747766 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 407.33ns
747768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof
747768 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns
747768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
750617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
750618 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1
751530 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1
751532 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 414.53ns
751533 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof
751533 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns
751534 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
754325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
754326 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2
755264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2
755267 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 457.23ns
755268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof
755268 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.61ns
755269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
758066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
758066 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3
759002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3
759004 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 647.95ns
759005 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof
759005 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.91ns
759006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
761873 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
761873 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall
762859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall
762984 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 122.86ms
762986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof
762987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.32ns
762989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
765878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s
765878 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists
766791 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists
766850 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.75ms
766851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof
766851 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.41ns
766853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
769909 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
769910 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2
770931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2
770933 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns
770968 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
771019 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight'
771039 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight'
771044 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop'
771051 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft''
771055 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft''
771056 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft''
771058 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
771062 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqNPermRange'
771064 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1'
771067 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft'
771068 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch'
771330 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft'
771332 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft'
771334 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1'
771337 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft'
771338 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch'
771493 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft'
771495 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft'
771496 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft'
771498 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2'
771500 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft'
771501 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch'
771714 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft'
771716 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
771718 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
771719 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2'
771720 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft'
771725 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch'
771922 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft'
771923 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
771925 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
771926 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1'
771927 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft'
771928 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch'
771937 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft'
771938 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
771939 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0'
771941 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1'
771944 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft'
771945 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch'
771955 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft'
771956 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft'
771957 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0'
771958 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv with='v_x_0''
771959 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft'
771960 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch'
772137 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv with='v_y_0''
772139 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft'
772140 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch'
772261 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0''
772263 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)''
772265 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight'
772267 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight'
772268 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight'
772270 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight'
772270 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap'
772273 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
772276 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm'
772278 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1'
772280 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0''
772280 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft'
772281 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch'
772388 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
772391 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight'
772393 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight'
772394 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft'
772395 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0''
772396 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft'
772398 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch'
772525 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap'
772527 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated'
772528 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0'
772529 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft'
772530 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft'
772531 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft'
772532 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0'
772534 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch'
772627 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0'
772629 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch'
772751 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch'
772755 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch'
772763 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap'
772764 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated'
772765 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0'
772768 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft'
772771 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft'
772772 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft'
772772 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0'
772780 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch'
772790 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch'
772797 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch'
772907 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap'
772909 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated'
772911 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0'
772913 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft'
772914 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft'
772914 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft'
772915 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0'
772916 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch'
772976 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch'
772983 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch'
773087 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]''
773090 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective'
773092 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0''
773094 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0''
773095 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft'
773096 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch'
773249 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch'
773253 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0''
773257 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)''
773259 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight'
773260 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight'
773261 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight'
773262 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight'
773263 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch'
773273 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm'
773279 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0''
773281 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1''
773282 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch'
773388 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight'
773390 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight'
773391 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft'
773392 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0''
773393 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft'
773395 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch'
773506 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap'
773508 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated'
773509 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0'
773511 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft'
773512 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft'
773513 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft'
773514 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0'
773515 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch'
773618 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0'
773620 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch'
773707 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0''
773708 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft'
773709 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch'
773714 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch'
773718 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch'
773724 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch'
773871 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap'
773874 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated'
773875 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0'
773876 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch'
773889 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch'
773986 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch'
778029 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 149: 'cut '(int)s_0[v_y_0] = v_y_0''
778030 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)''
778036 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight'
778038 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight'
778039 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight'
778039 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight'
778041 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch'
778053 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm'
778055 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0''
778057 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0''
778058 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft'
778058 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch'
778176 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch'
778180 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight'
778182 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight'
778182 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft'
778184 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0''
778185 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft'
778186 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch'
778305 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap'
778307 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated'
778308 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0'
778309 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft'
778310 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft'
778311 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft'
778311 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0'
778312 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch'
778400 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0'
778402 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch'
778488 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch'
778493 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch'
778497 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap'
778499 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated'
778500 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0'
778501 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch'
778512 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch'
778608 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap'
778609 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated'
778610 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0'
778611 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch'
778695 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch'
778706 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0''
778707 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)''
778709 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight'
778710 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight'
778711 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight'
778712 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight'
778712 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch'
778725 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm'
778727 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0''
778728 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0''
778729 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft'
778729 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch'
778832 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))''
778834 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0''
778835 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0''
778836 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft'
778837 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch'
778943 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch'
778948 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight'
778950 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight'
778951 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft'
778951 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0''
778952 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft'
778953 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch'
779069 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap'
779071 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated'
779073 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0'
779075 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft'
779076 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft'
779076 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft'
779077 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0'
779078 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap'
779079 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated'
779080 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0'
779082 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft'
779082 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft'
779083 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft'
779084 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0'
779085 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch'
779186 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0'
779188 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch'
779195 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch'
779286 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch'
779387 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split'
779388 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap'
779390 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated'
779391 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0'
779392 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft'
779393 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft'
779393 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft'
779394 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0'
779395 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch'
779498 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch'
779505 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch'
779610 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap'
779612 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated'
779612 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0'
779614 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft'
779614 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft'
779615 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft'
779615 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0'
779616 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch'
779622 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0'
779623 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch'
779717 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch'
779723 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch'
779729 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch'
779903 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap'
779904 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated'
779905 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0'
779906 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft'
779907 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft'
779907 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft'
779907 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0'
779908 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch'
779971 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0'
779972 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap'
779973 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated'
779974 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0'
779975 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch'
779981 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch'
779987 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch'
780123 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch'
780224 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap'
780226 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated'
780226 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0'
780227 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch'
780420 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch'
780521 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0''
780522 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch'
784138 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm'
784143 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1''
784145 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0''
784146 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft'
784147 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch'
784342 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))''
784343 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1''
784345 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0''
784346 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft'
784347 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch'
784470 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch'
787929 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch'
791874 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)''
791880 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0''
791881 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0''
791882 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft'
791883 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch'
792026 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))''
792028 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0''
792029 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1''
792031 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)' ...'
792032 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch'
793408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof
793409 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.81ns
793409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
796336 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
796336 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1
797313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1
797314 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns
797315 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
797324 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)''
797337 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x''
797340 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y''
797342 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft'
797343 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch'
797348 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft'
797350 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
797353 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1'
797356 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight'
797357 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch'
797368 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0''
797370 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight'
797370 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch'
797423 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight'
797424 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight'
797425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0''
797425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft'
797426 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch'
797501 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft'
797502 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange'
797503 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0''
797504 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft'
797505 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch'
797509 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
797510 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
797510 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange'
797511 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x''
797513 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft'
797513 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch'
797604 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
797605 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
797606 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange'
797608 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y''
797609 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft'
797609 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch'
797709 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
797710 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft'
797711 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0'
797712 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef'
797712 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0'
797714 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0'
797714 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0'
797715 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2'
797716 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft'
797717 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0'
797717 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0'
797718 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0'
797719 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0'
797719 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0'
797720 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0'
797721 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0'
797721 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0'
797722 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0'
797724 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch'
797726 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch'
797771 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0'
797773 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
797844 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0'
797846 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective'
797847 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0''
797849 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y''
797850 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft'
797851 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
797910 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch'
797913 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0'
797914 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective'
797916 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0''
797918 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x''
797919 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft'
797919 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch'
797976 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch'
797979 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch'
797983 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch'
798054 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch'
798127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof
798127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.92ns
798128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
801277 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s
801277 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq
802333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq
802374 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.61ms