373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key
400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.71ms
670 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
752 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)
2117 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
2119 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
2124 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
2125 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
3845 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
10957 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 10.29s
11045 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key
11091 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.2ns
11108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof
11110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.62ms
11116 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
14973 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s
14976 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut
16200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut
16233 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.56ms
16251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof
16251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 448.5ns
16254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
19766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s
19767 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight
20924 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight
20950 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.21ms
20956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof
20957 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.3ns
20959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
24394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s
24395 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1
25520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1
25528 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms
25531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof
25531 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.9ns
25532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
28928 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s
28929 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2
29981 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2
29987 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms
29990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof
29990 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.9ns
29992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
33216 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s
33216 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos
34254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos
34300 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.7ms
34303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof
34304 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.5ns
34305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
37514 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s
37515 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg
38580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg
38603 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.29ms
38607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof
38608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 382ns
38609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
41882 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s
41882 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt
42921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt
42926 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 873.4ns
42928 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof
42929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.6ns
42930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
46099 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s
46100 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong
47123 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong
47127 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.8ns
47129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof
47130 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.9ns
47131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
50329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s
50329 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort
51350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort
51353 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.9ns
51357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof
51358 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.1ns
51361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
54420 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
54421 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte
55413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte
55416 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707ns
55418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof
55418 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.1ns
55419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
58576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s
58577 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar
59737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar
59740 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 817ns
59743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof
59743 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 423ns
59745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
62923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s
62924 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1
63936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1
63986 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46ms
63990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof
63992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.12ms
63994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
67093 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s
67093 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2
68119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2
68192 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.77ms
68196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof
68196 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.1ns
68198 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
71287 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s
71287 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists
72315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists
72518 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.76ms
72523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof
72523 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.5ns
72524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
75626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s
75627 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one
76624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one
76630 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.39ms
76632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof
76633 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.91ms
76635 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
79810 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s
79811 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one
80819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one
80823 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms
80826 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof
80827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.4ns
80828 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
83931 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s
83932 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero
84924 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero
84985 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.8ms
84987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof
84988 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.8ns
84989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
88179 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s
88179 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1
89203 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1
89222 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.38ms
89225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof
89225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.8ns
89226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
92357 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s
92357 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2
93374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2
93396 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.23ms
93398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof
93400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns
93404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
96485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s
96486 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1
97499 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1
97516 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.36ms
97518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof
97518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.4ns
97520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
100602 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s
100603 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2
101582 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2
101599 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms
101602 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof
101602 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.7ns
101604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
104705 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s
104705 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1
105692 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1
105717 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.91ms
105719 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof
105719 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns
105720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
108827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s
108827 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2
109856 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2
109859 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms
109861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof
109861 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.5ns
109862 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
112980 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s
112980 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom
113994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom
114058 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.35ms
114060 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof
114060 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.1ns
114061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
117154 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s
117154 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus
118307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus
118369 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55ms
118372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof
118372 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.1ns
118373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
121478 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s
121478 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom
122517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom
122558 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.78ms
122561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof
122564 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.45ms
122566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
125566 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
125566 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos
126551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos
126559 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.68ms
126563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof
126564 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.08ms
126566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
129595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
129596 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg
130595 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg
130609 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.07ms
130611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof
130612 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.1ns
130613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
133569 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
133569 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos
134612 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos
134624 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.23ms
134626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof
134626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.1ns
134627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
137682 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
137682 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg
138677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg
138685 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.52ms
138686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof
138686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns
138687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
141795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s
141795 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos
142786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos
142798 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.91ms
142800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof
142800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns
142801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
145961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s
145961 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg
146937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg
146944 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms
146945 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof
146945 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.1ns
146946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
150008 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
150008 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero
150979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero
150983 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms
150984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof
150984 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns
150985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
154078 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s
154079 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum
155075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum
155091 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.28ms
155093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof
155093 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns
155094 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
158179 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s
158180 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom
159177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom
159222 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.16ms
159224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof
159225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.4ns
159226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
162338 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s
162339 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos
163333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos
163352 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.24ms
163355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof
163356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.4ns
163357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
166352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
166352 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg
167342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg
167361 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.69ms
167363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof
167363 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.1ns
167364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
170380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
170380 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos
171337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos
171366 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25ms
171369 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof
171370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.5ns
171371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
174362 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
174362 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg
175299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg
175318 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.8ms
175320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof
175320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.4ns
175322 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
178322 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
178323 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1
179267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1
179310 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.73ms
179312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof
179312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.7ns
179313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
182275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
182275 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2
183247 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2
183250 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms
183251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof
183251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns
183252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
186269 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
186270 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero
187237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero
187250 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms
187253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof
187256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.98ms
187257 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
190297 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
190298 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom
191273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom
191283 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.24ms
191284 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof
191284 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.1ns
191285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
194236 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
194236 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos
195172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos
195181 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.57ms
195182 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof
195182 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns
195183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
198180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
198180 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg
199134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg
199155 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.83ms
199156 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof
199157 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns
199157 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
202130 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
202130 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero
203099 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero
203108 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.52ms
203110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof
203110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns
203110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
206081 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
206081 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero
207073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero
207078 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms
207081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof
207081 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.4ns
207083 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
210078 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
210078 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum
211088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum
211092 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms
211094 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof
211094 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns
211094 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
214130 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
214130 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom
215121 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom
215127 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms
215129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof
215129 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.7ns
215131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
218129 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
218130 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1
219105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1
219185 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.71ms
219188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof
219188 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.8ns
219189 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
222239 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s
222240 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2
223232 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2
223339 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 96.49ms
223344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof
223344 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.7ns
223345 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
226268 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s
226269 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem
227221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem
227225 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms
227227 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof
227227 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.6ns
227231 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
230251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
230252 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod
231229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod
231281 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.52ms
231282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof
231282 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.8ns
231284 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
234376 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s
234376 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible
235362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible
235392 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.15ms
235393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof
235393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns
235394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
238410 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
238410 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep
239384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep
239387 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms
239390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof
239390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.7ns
239392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
242371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
242372 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom
243353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom
243514 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 148.55ms
243517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof
243517 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.7ns
243518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
246548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
246548 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero
247531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero
247542 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.89ms
247543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof
247543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns
247544 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
250640 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s
250640 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero
251602 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero
251616 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.44ms
251619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof
251619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.1ns
251620 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
254644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
254644 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero
255611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero
255630 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.74ms
255631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof
255632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns
255632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
258594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
258594 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom
259561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom
259575 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.32ms
259580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof
259580 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.5ns
259581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
262539 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
262539 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty
263487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty
263491 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms
263493 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof
263493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns
263493 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
266543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s
266543 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper
267482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper
267487 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms
267488 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof
267488 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns
267489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
270476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
270477 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower
271405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower
271425 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.35ms
271426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof
271427 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns
271427 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
274463 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
274463 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds
275411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds
275427 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.99ms
275428 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof
275428 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns
275429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
278455 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
278455 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2
279386 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2
279411 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.43ms
279412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof
279413 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns
279413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
282433 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
282433 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2
283416 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2
283420 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms
283421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof
283421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns
283422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
286371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
286371 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete
287314 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete
287318 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms
287319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof
287319 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns
287320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
290262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
290262 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2
291214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2
291220 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms
291221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof
291221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns
291222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
294149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
294149 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete
295088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete
295091 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms
295092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof
295092 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns
295093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
298027 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
298027 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete
299074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete
299076 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.6ns
299077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof
299077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns
299078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
302032 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
302033 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2
302992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2
302996 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms
302998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof
303003 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.92ms
303004 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
306006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
306006 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete
306997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete
306999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 942.6ns
307000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof
307001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns
307001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
309992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
309992 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive
310978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive
311020 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.64ms
311022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof
311022 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.3ns
311023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
314092 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s
314092 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound
315084 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound
315118 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.02ms
315120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof
315120 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns
315121 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
318186 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s
318186 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound
319156 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound
319187 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.97ms
319189 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof
319189 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns
319190 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
322252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
322252 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element
323226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element
323270 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.79ms
323272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof
323272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns
323273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
326274 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
326274 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index
327275 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index
327310 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.22ms
327312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof
327312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.7ns
327313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
330306 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
330307 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index
331286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index
331349 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.49ms
331351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof
331351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns
331351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
334351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
334351 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index
335317 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index
335346 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.83ms
335347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof
335347 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns
335348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
338386 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
338386 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max
339340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max
339360 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.45ms
339361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof
339361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns
339362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
342389 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
342389 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2
343371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2
343395 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.35ms
343397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof
343397 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns
343398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
346361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
346361 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3
347334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3
347353 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.07ms
347355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof
347355 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.8ns
347356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
350264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
350265 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4
351233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4
351258 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.74ms
351259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof
351259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns
351260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
354320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
354320 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max
355303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max
355331 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.14ms
355334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof
355334 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.6ns
355335 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
358321 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
358322 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2
359274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2
359303 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.23ms
359305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof
359305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.5ns
359306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
362305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
362305 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3
363259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3
363280 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.5ms
363282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof
363282 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns
363283 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
366301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
366301 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4
367262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4
367282 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.9ms
367283 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof
367283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns
367284 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
370326 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
370326 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0
371274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0
371295 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.19ms
371297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof
371298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.2ns
371298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
374365 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s
374365 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt
375391 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt
375412 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.4ms
375414 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof
375414 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns
375415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
378469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s
378469 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete
379420 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete
379428 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms
379429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof
379429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns
379430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
382457 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
382457 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive
383449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive
383470 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.71ms
383472 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof
383472 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns
383472 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
386535 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
386535 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split
387511 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split
387515 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms
387516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof
387516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns
387517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
390596 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s
390596 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0
391567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0
391570 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.1ns
391572 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof
391572 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.9ns
391573 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
394574 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
394574 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1
395550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1
395553 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 870.1ns
395554 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof
395554 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns
395555 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
398620 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s
398620 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor
399582 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor
399589 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms
399590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof
399590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns
399591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
402646 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s
402646 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd
403618 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd
403626 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms
403628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof
403628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.7ns
403629 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
406691 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
406691 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono
407671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono
407685 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.33ms
407686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof
407686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.6ns
407687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
410691 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
410691 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete
411708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete
411712 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms
411713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof
411713 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns
411714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
414843 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s
414843 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight
415814 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight
415816 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 602.2ns
415817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof
415817 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns
415818 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
418764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
418764 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive
419792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive
419799 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms
419800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof
419800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns
419801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
422785 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
422785 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete
423767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete
423769 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 696.9ns
423771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof
423771 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns
423771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
426815 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
426816 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete
427809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete
427812 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 675.9ns
427813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof
427813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns
427814 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
430951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s
430951 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower
431938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower
431941 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.6ns
431942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof
431942 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns
431943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
434941 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
434942 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper
435949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper
435953 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms
435954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof
435954 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns
435955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
439065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s
439066 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete
440092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete
440102 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.43ms
440103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof
440103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns
440104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
443127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
443127 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete
444104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete
444108 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms
444109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof
444109 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns
444110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
447075 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
447075 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct
448069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct
448076 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms
448077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof
448077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns
448078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
451103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
451104 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete
452042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete
452047 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms
452048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof
452048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns
452049 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
455167 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s
455167 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity
456181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity
456198 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms
456200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof
456200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns
456200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
459378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s
459378 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete
460421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete
460425 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms
460426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof
460426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns
460427 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
463548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s
463548 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity
464564 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity
464572 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.79ms
464575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof
464575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.6ns
464576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
467646 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s
467646 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete
468644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete
468649 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms
468650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof
468650 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns
468651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
471675 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
471676 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive
472648 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive
472664 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.38ms
472665 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof
472665 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns
472666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
475671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s
475671 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete
476613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete
476618 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 362.2ns
476621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof
476623 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.62ms
476624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
479582 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
479582 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono
480581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono
480614 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.97ms
480616 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof
480616 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.7ns
480616 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
483653 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
483653 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete
484590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete
484594 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms
484595 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof
484595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns
484596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
487592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
487592 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess
488549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess
488570 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.04ms
488574 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof
488574 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.7ns
488575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
491573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
491573 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2
492552 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2
492570 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.71ms
492572 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof
492572 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns
492573 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
495524 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
495524 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow
496490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow
496544 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.76ms
496546 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof
496546 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns
496547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
499583 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
499583 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete
500535 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete
500538 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 510.8ns
500539 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof
500539 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns
500540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
503472 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
503473 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze
504417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze
504423 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms
504424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof
504424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns
504425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
507397 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
507397 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals
508422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals
508426 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms
508428 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof
508428 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205ns
508429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
511404 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
511404 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1
512346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1
512348 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 753.3ns
512350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof
512350 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns
512350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
515340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
515341 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2
516297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2
516300 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.8ns
516302 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof
516303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.7ns
516304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
519345 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
519345 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1
520328 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1
520331 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms
520333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof
520333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns
520334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
523417 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s
523417 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2
524441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2
524443 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms
524445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof
524445 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns
524445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
527489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
527489 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges
528452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges
528460 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.35ms
528462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof
528462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns
528462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
531427 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
531427 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1
532436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1
532445 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.91ms
532447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof
532447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns
532448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
535386 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
535386 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2
536389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2
536396 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms
536397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof
536398 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns
536398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
539383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
539383 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition
540420 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition
540432 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.75ms
540434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof
540434 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns
540435 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
543418 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
543418 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue
544416 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue
544420 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms
544421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof
544421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns
544422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
547361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
547361 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny
548348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny
548352 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms
548353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof
548353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns
548354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
551358 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
551359 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast
552346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast
552348 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 914.1ns
552349 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof
552349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns
552350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
555293 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
555293 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton
556268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton
556271 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 966.8ns
556272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof
556272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns
556273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
559214 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
559214 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete
560210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete
560212 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 960.1ns
560214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof
560214 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.6ns
560215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
563211 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
563211 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat
564182 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat
564194 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.71ms
564195 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof
564195 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns
564196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
567129 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
567129 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub
568112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub
568115 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms
568116 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof
568116 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns
568117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
571091 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
571091 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse
572071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse
572077 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms
572079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof
572079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.1ns
572080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
575114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
575114 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty
576107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty
576109 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.9ns
576110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof
576110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns
576111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
579031 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s
579032 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton
579992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton
579994 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 634.4ns
579995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof
579995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns
579996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
582949 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
582950 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat
583933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat
583937 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms
583938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof
583938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns
583939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
586893 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
586894 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub
587877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub
587880 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms
587881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof
587881 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns
587882 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
590816 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
590816 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse
591804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse
591807 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms
591808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof
591808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns
591809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
594768 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
594768 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft
595790 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft
595793 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms
595794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof
595795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns
595795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
598737 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
598738 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight
599726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight
599731 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms
599733 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof
599733 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.5ns
599734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
602710 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
602710 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ
603681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ
603684 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms
603685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof
603685 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns
603686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
606689 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
606689 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ
607693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ
607704 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.08ms
607705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof
607705 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns
607705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
610655 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
610655 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ
611586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ
611588 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 597.3ns
611589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof
611590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns
611590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
614500 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
614500 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ
615473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ
615480 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms
615482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof
615482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns
615483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
618481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
618481 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ
619485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ
619488 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 880ns
619490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof
619490 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns
619490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
622453 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
622453 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ
623440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ
623442 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 782.2ns
623443 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof
623443 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns
623444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
626470 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
626470 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ
627445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ
627449 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms
627450 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof
627450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns
627451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
630493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
630493 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ
631474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ
631476 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 994.5ns
631477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof
631477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns
631478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
634450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
634450 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ
635433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ
635436 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms
635437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof
635437 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns
635438 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
638426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
638427 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ
639403 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ
639406 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms
639408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof
639408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.2ns
639409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
642472 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
642472 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ
643482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ
643486 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms
643487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof
643487 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns
643488 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
646528 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
646529 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1
647492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1
647501 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ms
647502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof
647502 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns
647503 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
650484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
650484 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2
651480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2
651489 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms
651490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof
651490 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns
651491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
654403 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s
654403 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty
655385 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty
655393 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms
655394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof
655394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns
655395 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
658376 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
658376 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete
659348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete
659356 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms
659357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof
659357 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns
659358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
662384 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
662384 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR
663378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR
663392 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.89ms
663393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof
663393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns
663394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
666309 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s
666309 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL
667289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL
667301 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.17ms
667303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof
667303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns
667304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
670292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
670293 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR
671248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR
671259 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.95ms
671260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof
671260 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns
671261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
674249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
674249 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL
675258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL
675266 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.37ms
675267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof
675267 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns
675268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
678231 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s
678231 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split
679214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split
679241 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.77ms
679243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof
679243 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns
679243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
682220 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
682220 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper
683224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper
683257 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.88ms
683259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof
683259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns
683260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
686246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
686246 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete
687239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete
687265 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.87ms
687267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof
687267 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.5ns
687268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
690258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
690259 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower
691276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower
691300 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.08ms
691302 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof
691303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.7ns
691304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
694322 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
694322 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete
695349 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete
695376 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.15ms
695378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof
695378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns
695379 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
698333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
698334 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three
699318 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three
699381 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.59ms
699383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof
699383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns
699384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
702361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
702362 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty
703360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty
703365 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms
703366 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof
703366 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns
703367 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
706381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s
706381 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand
707350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand
707356 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms
707358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof
707358 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233ns
707359 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
710291 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
710292 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper
711277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper
711282 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms
711283 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof
711283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns
711284 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
714327 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
714327 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq
715346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq
715364 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.36ms
715366 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof
715366 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns
715367 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
718412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s
718412 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2
719395 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2
719403 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms
719404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof
719404 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.2ns
719405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
722454 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s
722454 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton
723480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton
723484 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms
723485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof
723485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns
723486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
726542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
726542 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst
727582 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst
727594 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.85ms
727596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof
727596 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns
727596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
730606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s
730606 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond
731609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond
731622 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.44ms
731623 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof
731623 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns
731624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
734658 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
734658 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub
735657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub
735675 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.48ms
735676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof
735676 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns
735677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
738788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s
738788 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq
739772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq
739775 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms
739776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof
739776 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns
739777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
742750 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
742750 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq
743758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq
743761 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms
743763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof
743763 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns
743763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
746757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
746757 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq
747752 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq
747759 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms
747760 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof
747760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns
747761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
750861 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s
750861 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv
751839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv
751845 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms
751846 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof
751846 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns
751847 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
754844 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
754844 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange
755836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange
755927 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.46ms
755929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof
755929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns
755929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
758905 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
758905 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans
759898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans
759922 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.82ms
759924 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof
759924 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.9ns
759925 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
762999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s
762999 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl
763969 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl
763983 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms
763984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof
763984 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns
763985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
766994 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s
766994 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit
768009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit
768011 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 283.2ns
768013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof
768013 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.5ns
768014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
770982 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
770983 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight
772037 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight
772149 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.37ms
772152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof
772152 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.5ns
772153 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
775123 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s
775123 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap
776114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap
776160 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.56ms
776161 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof
776162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns
776162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
779169 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s
779169 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0
780215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0
780217 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 344.5ns
780219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof
780219 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns
780219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
783241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
783241 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1
784226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1
784228 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 281.7ns
784229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof
784229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns
784230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
787227 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s
787227 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2
788224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2
788226 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 269ns
788227 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof
788227 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns
788228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
791169 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
791169 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3
792129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3
792132 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 566.6ns
792133 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof
792133 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns
792134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
795142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s
795142 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall
796112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall
796229 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.68ms
796232 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof
796232 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.6ns
796233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
799258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
799258 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists
800243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists
800299 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.59ms
800300 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof
800300 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns
800302 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
803324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
803325 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2
804365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2
804366 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns
804403 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
804464 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight'
804486 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight'
804493 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop'
804508 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft''
804510 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft''
804512 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft''
804514 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
804521 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqNPermRange'
804522 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1'
804527 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft'
804529 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch'
804765 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft'
804766 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft'
804768 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1'
804769 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft'
804771 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch'
804895 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft'
804897 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft'
804898 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft'
804899 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2'
804901 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft'
804903 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch'
805093 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft'
805094 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
805096 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
805096 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2'
805097 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft'
805098 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch'
805250 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft'
805252 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
805254 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
805257 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1'
805257 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft'
805259 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch'
805267 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft'
805268 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
805269 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0'
805271 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1'
805272 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft'
805274 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch'
805284 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft'
805285 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft'
805287 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0'
805288 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv with='v_x_0''
805289 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft'
805290 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch'
805447 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv with='v_y_0''
805448 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft'
805449 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch'
805604 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0''
805606 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)''
805607 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight'
805610 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight'
805611 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight'
805612 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight'
805613 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap'
805614 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
805619 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm'
805620 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1'
805621 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0''
805622 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft'
805623 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch'
805748 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
805753 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight'
805754 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight'
805755 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft'
805756 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0''
805757 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft'
805758 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch'
805900 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap'
805902 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated'
805903 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0'
805905 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft'
805907 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft'
805908 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft'
805909 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0'
805910 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch'
806035 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0'
806036 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch'
806190 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch'
806199 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch'
806208 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap'
806209 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated'
806210 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0'
806212 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft'
806213 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft'
806213 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft'
806214 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0'
806215 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch'
806229 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch'
806236 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch'
806344 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap'
806346 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated'
806347 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0'
806349 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft'
806349 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft'
806350 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft'
806351 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0'
806352 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch'
806408 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch'
806415 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch'
806533 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]''
806535 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective'
806536 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0''
806538 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0''
806540 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft'
806541 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch'
806723 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch'
806728 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0''
806729 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)''
806731 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight'
806732 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight'
806733 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight'
806734 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight'
806735 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch'
806795 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm'
806796 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0''
806798 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1''
806799 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch'
806918 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight'
806919 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight'
806920 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft'
806927 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0''
806927 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft'
806928 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch'
807045 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap'
807046 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated'
807048 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0'
807049 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft'
807050 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft'
807050 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft'
807051 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0'
807052 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch'
807137 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0'
807139 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch'
807221 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0''
807221 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft'
807222 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch'
807227 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch'
807231 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch'
807236 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch'
807370 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap'
807371 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated'
807372 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0'
807373 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch'
807384 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch'
807473 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch'
811366 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 149: 'cut '(int)s_0[v_y_0] = v_y_0''
811367 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)''
811371 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight'
811373 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight'
811373 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight'
811374 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight'
811374 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch'
811382 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm'
811383 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0''
811384 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0''
811385 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft'
811386 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch'
811481 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch'
811485 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight'
811486 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight'
811486 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft'
811487 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0''
811488 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft'
811488 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch'
811597 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap'
811598 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated'
811599 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0'
811600 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft'
811601 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft'
811601 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft'
811602 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0'
811603 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch'
811684 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0'
811685 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch'
811770 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch'
811775 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch'
811780 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap'
811781 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated'
811781 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0'
811782 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch'
811793 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch'
811885 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap'
811886 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated'
811886 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0'
811887 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch'
811967 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch'
811978 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0''
811978 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)''
811979 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight'
811981 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight'
811981 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight'
811981 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight'
811982 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch'
811994 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm'
811994 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0''
811995 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0''
811996 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft'
811997 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch'
812088 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))''
812089 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0''
812090 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0''
812090 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft'
812091 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch'
812192 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch'
812197 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight'
812198 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight'
812199 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft'
812200 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0''
812200 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft'
812201 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch'
812307 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap'
812308 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated'
812309 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0'
812310 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft'
812311 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft'
812311 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft'
812312 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0'
812312 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap'
812313 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated'
812314 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0'
812315 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft'
812315 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft'
812316 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft'
812316 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0'
812317 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch'
812416 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0'
812417 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch'
812425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch'
812513 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch'
812605 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split'
812606 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap'
812607 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated'
812608 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0'
812609 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft'
812609 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft'
812610 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft'
812611 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0'
812611 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch'
812615 WARN Test worker d.u.i.k.p.i.ApplyStrategy doWork exception java.lang.AssertionError: Formula Term top level of equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,jv_0),int::seqGet(s_0,v_x_0),if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))) does not exist
at de.uka.ilkd.key.strategy.BuiltInRuleAppContainer.<init>(BuiltInRuleAppContainer.java:42)
812616 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch'
812616 WARN Test worker d.u.i.k.p.i.ApplyStrategy doWork exception java.lang.AssertionError: Formula Term top level of equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,jv_0),int::seqGet(s_0,v_x_0),if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))) does not exist
at de.uka.ilkd.key.strategy.BuiltInRuleAppContainer.<init>(BuiltInRuleAppContainer.java:42)
812616 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch'
812616 WARN Test worker d.u.i.k.p.i.ApplyStrategy doWork exception java.lang.AssertionError: Formula Term top level of equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,jv_0),int::seqGet(s_0,v_x_0),if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))) does not exist
at de.uka.ilkd.key.strategy.BuiltInRuleAppContainer.<init>(BuiltInRuleAppContainer.java:42)
812617 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap'
812617 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine GOALS: 8
812618 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),exists{v_r:Seq}(and(and(and(and(equals(seqLen(v_r),seqLen(f_s)),seqNPerm(v_r)),all{v_iv:int}(imp(and(leq(Z(0(#)),v_iv),lt(v_iv,seqLen(f_s))),equals(any::seqGet(f_s,v_iv),any::seqGet(f_t,int::seqGet(v_r,v_iv)))))),equals(int::seqGet(v_r,v_x_0),v_x_0)),equals(int::seqGet(v_r,v_y_0),v_y_0)))]
812619 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(int::seqGet(seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0),v_y_0),v_y_0)]
812619 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(int::seqGet(seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0),v_x_0),v_x_0)]
812619 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),and(and(and(leq(Z(0(#)),jv_0),leq(Z(0(#)),v_y_0)),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0)))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0)))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(seqSwap(s_0,jv_0,v_x_0),v_iv_0)))]
812619 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),equals(v_iv_0,v_y_0),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(seqSwap(s_0,jv_0,v_x_0),v_iv_0)))]
812619 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [equals(v_iv_0,v_y_0),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),and(and(and(leq(Z(0(#)),jv_0),leq(Z(0(#)),v_x_0)),lt(jv_0,seqLen(s_0))),lt(v_x_0,seqLen(s_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,jv_0)))]
812620 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [equals(jv_0,jv_0),lt(v_x_0,seqLen(s_0)),equals(v_iv_0,v_y_0),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0)))]
812620 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [lt(v_x_0,seqLen(s_0)),equals(v_iv_0,v_y_0),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),equals(jv_0,jv_0),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))]
812627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof
812627 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns
812630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
815893 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s
815893 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1
816916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1
816917 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns
816918 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop'
816927 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)''
816937 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x''
816940 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y''
816943 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft'
816945 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch'
816951 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft'
816951 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop'
816957 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1'
816957 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight'
816960 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch'
816972 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0''
816972 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight'
816974 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch'
817032 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight'
817033 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight'
817034 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0''
817035 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft'
817035 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch'
817114 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft'
817115 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange'
817115 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0''
817116 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft'
817117 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch'
817122 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft'
817122 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft'
817123 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange'
817123 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x''
817124 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft'
817125 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch'
817231 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft'
817231 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft'
817232 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange'
817233 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y''
817234 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft'
817234 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch'
817335 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft'
817336 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft'
817336 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0'
817337 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef'
817338 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0'
817339 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0'
817339 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0'
817340 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2'
817341 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft'
817341 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0'
817342 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0'
817342 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0'
817342 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0'
817343 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0'
817344 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0'
817344 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0'
817345 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0'
817346 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0'
817347 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch'
817350 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch'
817397 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0'
817398 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch'
817462 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0'
817463 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective'
817464 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0''
817465 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y''
817466 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft'
817466 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch'
817562 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch'
817564 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0'
817565 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective'
817566 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0''
817567 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x''
817568 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft'
817575 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch'
817637 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch'
817639 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch'
817643 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch'
817712 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch'
817783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof
817783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.8ns
817784 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
820939 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s
820939 INFO Test worker d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq
822044 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq
822068 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.37ms