Class de.uka.ilkd.key.proof.proverules.ProveRulesTest

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
198
tests
failures
ignored
11m26.89s
duration
100%
successful
Tests
Standard output
Tests

Test	Method name	Duration	Result
powPositive	data()[100]	3.342s	passed
powPositiveConcrete	data()[101]	3.331s	passed
powGeq1Concrete	data()[102]	3.337s	passed
pow2InIntLower	data()[103]	3.331s	passed
pow2InIntUpper	data()[104]	3.348s	passed
logSelfConcrete	data()[105]	3.336s	passed
log1Concrete	data()[106]	3.336s	passed
logProduct	data()[107]	3.341s	passed
logTimesBaseConcrete	data()[108]	3.325s	passed
logProdIdentity	data()[109]	3.335s	passed
moduloByteIsInByte	data()[10]	3.416s	passed
logProdIdentityConcrete	data()[110]	3.321s	passed
logPowIdentity	data()[111]	3.328s	passed
logPowIdentityConcrete	data()[112]	3.320s	passed
logPositive	data()[113]	3.357s	passed
logPositiveConcrete	data()[114]	3.325s	passed
logMono	data()[115]	3.354s	passed
logMonoConcrete	data()[116]	3.329s	passed
powLogLess	data()[117]	3.342s	passed
powLogMore2	data()[118]	3.359s	passed
logLessThanPow	data()[119]	3.352s	passed
moduloCharIsInChar	data()[11]	3.420s	passed
logLessThanPowConcrete	data()[120]	3.326s	passed
logSqueeze	data()[121]	3.320s	passed
ifthenelse_equals	data()[122]	3.354s	passed
ifthenelse_equals_1	data()[123]	3.332s	passed
ifthenelse_equals_2	data()[124]	3.331s	passed
disjointWithSingleton1	data()[125]	3.332s	passed
disjointWithSingleton2	data()[126]	3.332s	passed
disjointArrayRanges	data()[127]	3.331s	passed
disjointArrayRangeAllFields1	data()[128]	3.367s	passed
disjointArrayRangeAllFields2	data()[129]	3.345s	passed
div_unique1	data()[12]	3.488s	passed
seqSelfDefinition	data()[130]	3.345s	passed
seqOutsideValue	data()[131]	3.341s	passed
castedGetAny	data()[132]	3.334s	passed
seqGetAlphaCast	data()[133]	3.364s	passed
getOfSeqSingleton	data()[134]	3.339s	passed
getOfSeqSingletonConcrete	data()[135]	3.338s	passed
getOfSeqConcat	data()[136]	3.345s	passed
getOfSeqSub	data()[137]	3.361s	passed
getOfSeqReverse	data()[138]	3.342s	passed
lenOfSeqEmpty	data()[139]	3.338s	passed
div_unique2	data()[13]	3.536s	passed
lenOfSeqSingleton	data()[140]	3.327s	passed
lenOfSeqConcat	data()[141]	3.370s	passed
lenOfSeqSub	data()[142]	3.333s	passed
lenOfSeqReverse	data()[143]	3.331s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.349s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.331s	passed
getOfSeqSingletonEQ	data()[146]	3.332s	passed
getOfSeqConcatEQ	data()[147]	3.365s	passed
getOfSeqSubEQ	data()[148]	3.330s	passed
getOfSeqReverseEQ	data()[149]	3.350s	passed
div_exists	data()[14]	3.561s	passed
lenOfSeqEmptyEQ	data()[150]	3.339s	passed
lenOfSeqSingletonEQ	data()[151]	3.330s	passed
lenOfSeqConcatEQ	data()[152]	3.363s	passed
lenOfSeqSubEQ	data()[153]	3.334s	passed
lenOfSeqReverseEQ	data()[154]	3.362s	passed
getOfSeqDefEQ	data()[155]	3.344s	passed
lenOfSeqDefEQ	data()[156]	3.352s	passed
seqConcatWithSeqEmpty1	data()[157]	3.362s	passed
seqConcatWithSeqEmpty2	data()[158]	3.402s	passed
seqReverseOfSeqEmpty	data()[159]	3.348s	passed
div_one	data()[15]	3.388s	passed
subSeqComplete	data()[160]	3.365s	passed
subSeqTailR	data()[161]	3.363s	passed
subSeqTailL	data()[162]	3.377s	passed
subSeqTailEQR	data()[163]	3.380s	passed
subSeqTailEQL	data()[164]	3.375s	passed
seqDef_split	data()[165]	3.371s	passed
seqDef_induction_upper	data()[166]	3.401s	passed
seqDef_induction_upper_concrete	data()[167]	3.381s	passed
seqDef_induction_lower	data()[168]	3.404s	passed
seqDef_induction_lower_concrete	data()[169]	3.396s	passed
jdiv_one	data()[16]	3.379s	passed
seqDef_split_in_three	data()[170]	3.456s	passed
seqDef_empty	data()[171]	3.386s	passed
seqDef_one_summand	data()[172]	3.362s	passed
seqDef_lower_equals_upper	data()[173]	3.350s	passed
seqDefOfSeq	data()[174]	3.372s	passed
seqSelfDefinitionEQ2	data()[175]	3.364s	passed
indexOfSeqSingleton	data()[176]	3.339s	passed
indexOfSeqConcatFirst	data()[177]	3.369s	passed
indexOfSeqConcatSecond	data()[178]	3.367s	passed
indexOfSeqSub	data()[179]	3.362s	passed
div_zero	data()[17]	3.411s	passed
lenOfArray2seq	data()[180]	3.349s	passed
getAnyOfArray2seq	data()[181]	3.347s	passed
getOfArray2seq	data()[182]	3.352s	passed
getAnyOfNPermInv	data()[183]	3.341s	passed
seqNPermRange	data()[184]	3.411s	passed
seqPermTrans	data()[185]	3.389s	passed
seqPermRefl	data()[186]	3.366s	passed
seqPermSplit	data()[187]	3.353s	passed
seqNPermRight	data()[188]	3.544s	passed
seqPermFromSwap	data()[189]	3.412s	passed
divResZero1	data()[18]	3.388s	passed
seqPermTransAlt0	data()[190]	3.340s	passed
seqPermTransAlt1	data()[191]	3.362s	passed
seqPermTransAlt2	data()[192]	3.345s	passed
seqPermTransAlt3	data()[193]	3.346s	passed
seqPermForall	data()[194]	3.453s	passed
seqPermExists	data()[195]	3.415s	passed
schiffl_lemma_2	data()[196]	21.379s	passed
schiffl_thm_1	data()[197]	4.088s	passed
eqSameSeq	data()[198]	3.507s	passed
divResZero2	data()[19]	3.399s	passed
eqTermCut	data()[1]	4.172s	passed
divResOne1	data()[20]	3.387s	passed
divResOne2	data()[21]	3.382s	passed
div_cancel1	data()[22]	3.404s	passed
div_cancel2	data()[23]	3.389s	passed
divAddMultDenom	data()[24]	3.421s	passed
divMinus	data()[25]	3.406s	passed
divMinusDenom	data()[26]	3.426s	passed
divLeastDPos	data()[27]	3.356s	passed
divLeastDNeg	data()[28]	3.347s	passed
divGreatestDPos	data()[29]	3.366s	passed
equivAllRight	data()[2]	3.780s	passed
divGreatestDNeg	data()[30]	3.346s	passed
divIncreasingPos	data()[31]	3.349s	passed
divIncreasingNeg	data()[32]	3.369s	passed
jdiv_zero	data()[33]	3.357s	passed
jdivPulloutMinusNum	data()[34]	3.370s	passed
jdivPulloutMinusDenom	data()[35]	3.401s	passed
jdiv_uniquePosPos	data()[36]	3.367s	passed
jdiv_uniquePosNeg	data()[37]	3.378s	passed
jdiv_uniqueNegPos	data()[38]	3.352s	passed
jdiv_uniqueNegNeg	data()[39]	3.378s	passed
irrflConcrete1	data()[3]	3.639s	passed
jdivMultDenom1	data()[40]	3.374s	passed
jdivMultDenom2	data()[41]	3.363s	passed
mod_geZero	data()[42]	3.370s	passed
mod_lessDenom	data()[43]	3.367s	passed
jmod_NumPos	data()[44]	3.333s	passed
jmod_NumNeg	data()[45]	3.359s	passed
jmod_geZero	data()[46]	3.333s	passed
jmodNumZero	data()[47]	3.329s	passed
jmod_pulloutminusNum	data()[48]	3.337s	passed
jmod_pulloutminusDenom	data()[49]	3.328s	passed
irrflConcrete2	data()[4]	3.571s	passed
jmodUnique1	data()[50]	3.445s	passed
jmodUnique2	data()[51]	3.435s	passed
intDivRem	data()[52]	3.341s	passed
jmodjmod	data()[53]	3.358s	passed
jmodDivisible	data()[54]	3.352s	passed
jmodDivisibleRep	data()[55]	3.324s	passed
jdivAddMultDenom	data()[56]	3.472s	passed
jmodAltZero	data()[57]	3.357s	passed
jmodAddMultDenomZero	data()[58]	3.353s	passed
polyDiv_zero	data()[59]	3.338s	passed
cancel_gtPos	data()[5]	3.565s	passed
polyMod_ltdivDenom	data()[60]	3.344s	passed
bsum_empty	data()[61]	3.329s	passed
bsum_induction_upper	data()[62]	3.328s	passed
bsum_induction_lower	data()[63]	3.348s	passed
bsum_num_of_bounds	data()[64]	3.347s	passed
bsum_num_of_bounds2	data()[65]	3.342s	passed
bsum_induction_upper2	data()[66]	3.350s	passed
bsum_induction_upper_concrete	data()[67]	3.341s	passed
bsum_induction_upper_concrete_2	data()[68]	3.359s	passed
bsum_induction_upper2_concrete	data()[69]	3.333s	passed
cancel_gtNeg	data()[6]	3.544s	passed
bsum_induction_lower_concrete	data()[70]	3.334s	passed
bsum_induction_lower2	data()[71]	3.325s	passed
bsum_induction_lower2_concrete	data()[72]	3.326s	passed
bsum_positive	data()[73]	3.401s	passed
bsum_upper_bound	data()[74]	3.379s	passed
bsum_lower_bound	data()[75]	3.359s	passed
bsum_positive_lower_bound_element	data()[76]	3.379s	passed
bsum_sub_same_index	data()[77]	3.392s	passed
bsum_less_same_index	data()[78]	3.411s	passed
bsum_equal_except_one_index	data()[79]	3.351s	passed
moduloIntIsInInt	data()[7]	3.423s	passed
bsum_num_of_is_max	data()[80]	3.342s	passed
bsum_num_of_is_max2	data()[81]	3.344s	passed
bsum_num_of_is_max3	data()[82]	3.350s	passed
bsum_num_of_is_max4	data()[83]	3.365s	passed
bsum_num_of_lt_max	data()[84]	3.375s	passed
bsum_num_of_lt_max2	data()[85]	3.381s	passed
bsum_num_of_lt_max3	data()[86]	3.366s	passed
bsum_num_of_lt_max4	data()[87]	3.358s	passed
bsum_num_of_gt0	data()[88]	3.364s	passed
bsum_num_of_gt0_alt	data()[89]	3.347s	passed
moduloLongIsInLong	data()[8]	3.427s	passed
bsum_add_concrete	data()[90]	3.327s	passed
bprod_all_positive	data()[91]	3.335s	passed
bprod_split	data()[92]	3.315s	passed
powConcrete0	data()[93]	3.321s	passed
powConcrete1	data()[94]	3.339s	passed
powSplitFactor	data()[95]	3.334s	passed
powAdd	data()[96]	3.342s	passed
powMono	data()[97]	3.344s	passed
powMonoConcrete	data()[98]	3.345s	passed
powMonoConcreteRight	data()[99]	3.326s	passed
moduloShortIsInShort	data()[9]	3.408s	passed
Standard output

271        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
292        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.14ms 
491        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506        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)

1387       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1390       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1393       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1393       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2628       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7863       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.37s 
7974       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8008       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.6ns 
8021       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8023       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.73ms 
8027       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11095      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
11098      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12184      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.85ms 
12199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12200      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 523.2ns 
12201      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15011      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
15012      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15976      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
15979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15980      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.9ns 
15981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18755      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
18756      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19616      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
19619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19619      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.3ns 
19621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
22310      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23187      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
23190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23191      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 494.4ns 
23192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25852      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
25852      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26753      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.23ms 
26754      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26755      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.4ns 
26756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
29419      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30277      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30297      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.24ms 
30299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.4ns 
30300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32873      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
32874      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33717      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33720      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703.91ns 
33723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33723      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.6ns 
33724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36303      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
36303      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37147      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 645.4ns 
37149      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37150      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.4ns 
37151      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39697      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
39698      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40552      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40555      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.7ns 
40557      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40558      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.4ns 
40559      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43125      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
43126      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43971      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.61ns 
43973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43973      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.7ns 
43974      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46578      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
46578      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
47388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
47391      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 519.4ns 
47403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
47403      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.8ns 
47405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50040      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
50040      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
50849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50889      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.49ms 
50891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50891      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.9ns 
50892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53553      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
53554      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
54367      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
54425      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.23ms 
54427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
54427      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.6ns 
54428      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57007      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
57007      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
57839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
57985      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 137.08ms 
57989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
57989      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.7ns 
57990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60529      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
60529      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
61369      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
61375      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
61379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
61380      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 909.21ns 
61381      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63915      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
63916      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
64752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
64755      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
64759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
64759      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.2ns 
64760      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67284      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
67285      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
68130      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
68167      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.79ms 
68169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
68169      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
68170      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70706      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
70706      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
71539      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
71555      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
71557      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
71558      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.2ns 
71559      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
74094      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
74938      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
74954      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.43ms 
74955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
74956      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.8ns 
74957      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
77517      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
78326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
78341      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.16ms 
78342      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
78342      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
78343      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
80893      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
81708      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
81723      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
81726      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
81726      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.8ns 
81727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84292      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
84293      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
85101      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
85127      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.66ms 
85130      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
85130      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.1ns 
85131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87679      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
87679      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
88512      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
88517      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
88520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
88520      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.9ns 
88522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91063      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
91063      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
91898      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
91937      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.85ms 
91940      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
91940      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.4ns 
91941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94458      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
94459      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
95288      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
95344      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.72ms 
95354      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
95355      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390ns 
95356      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97898      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
97898      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
98727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
98769      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.91ms 
98772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
98772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.7ns 
98773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
101289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
102118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
102126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
102128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
102129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289ns 
102130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
104638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
105461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
105473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.91ms 
105474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
105474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
105476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
108022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
108829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
108839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.15ms 
108840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
108841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
108841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
111375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
112178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
112185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
112186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
112186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
112187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
114726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
115527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
115534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
115535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
115536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
115536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
118071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
118897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
118903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
118905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
118905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
118906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
121422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
122257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
122261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
122262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
122262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
122263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
124796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
125620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
125630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.74ms 
125632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
125632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
125633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
128143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
128976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
129031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.76ms 
129033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
129033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
129033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
131550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
132377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
132398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.84ms 
132401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
132401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.6ns 
132403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
134936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
135759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
135776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.91ms 
135778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
135778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 
135779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
138310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
139111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
139129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.05ms 
139130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
139130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
139131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
141659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
142489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
142506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ms 
142508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
142508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.6ns 
142508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
145041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
145841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
145880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.55ms 
145882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
145882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
145883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
148413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
149238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
149244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
149245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
149245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
149246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
151772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
152608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
152613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
152615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
152615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.4ns 
152616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
155147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
155972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
155980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.55ms 
155981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
155982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
155982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
158483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
159304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
159313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.28ms 
159314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
159314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
159315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
161813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
162638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
162668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.28ms 
162675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
162675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300ns 
162676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
165176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
165996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
166005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.59ms 
166007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
166007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.6ns 
166008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
168505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
169331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
169334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
169336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
169337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.1ns 
169338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
171870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
172668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
172671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
172673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
172673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
172673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
175194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
175991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
175999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ms 
176001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
176001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
176002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
178520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
179358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
179444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.14ms 
179446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
179447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.5ns 
179448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
181958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
182796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
182879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.64ms 
182881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
182881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
182881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
185394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
186217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
186220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
186222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
186222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.6ns 
186223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
188718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
189541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
189578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.75ms 
189580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
189580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.8ns 
189581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
192076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
192901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
192930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.49ms 
192932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
192932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
192932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
195426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
196251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
196254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
196255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
196255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
196256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
198778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
199583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
199726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 130.76ms 
199728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
199728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.2ns 
199729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
202271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
203073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
203084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ms 
203085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
203085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
203086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
205603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
206428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
206436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.96ms 
206437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
206437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
206438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
208935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
209758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
209774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.56ms 
209776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
209776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.6ns 
209777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
212279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
213099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
213113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.52ms 
213120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
213120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.1ns 
213121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
215629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
216442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
216447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
216449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
216450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.4ns 
216450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
218943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
219770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
219775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
219777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
219777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
219777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
222281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
223100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
223123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.37ms 
223125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
223125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
223126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
225626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
226453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
226470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.08ms 
226471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
226471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
226472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
228998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
229797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
229812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms 
229813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
229814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.8ns 
229814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
232357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
233159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
233162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
233163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
233163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
233164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
235694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
236498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
236503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
236506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
236506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283ns 
236507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
239036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
239858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
239863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
239864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
239864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
239865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
242373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
243194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
243197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
243198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
243198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
243199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
245707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
246528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
246530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 685.8ns 
246532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
246532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
246532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
249032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
249852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
249856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
249857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
249857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
249858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
252361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
253179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
253182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 958.71ns 
253183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
253183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
253184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
255685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
256513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
256582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.6ms 
256584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
256584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
256585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
259103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
259923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
259961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.12ms 
259962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
259963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
259963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
262495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
263292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
263321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.41ms 
263322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
263322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
263323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
265861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
266658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
266699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.51ms 
266701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
266701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
266701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
269238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
270061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
270092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.77ms 
270093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
270093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
270094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
272629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
273452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
273502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.1ms 
273503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
273503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
273504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
276004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
276826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
276853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.07ms 
276854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
276854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
276855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
279355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
280175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
280196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.3ms 
280197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
280197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
280198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
282695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
283515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
283539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.5ms 
283541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
283541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
283541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
286031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
286869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
286889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.64ms 
286890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
286890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
286891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
289424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
290225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
290254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.13ms 
290256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
290256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.3ns 
290257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
292799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
293603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
293629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.69ms 
293630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
293630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
293634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
296159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
296985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
297010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.16ms 
297011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
297012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
297012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
299529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
300351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
300376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.03ms 
300377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
300377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
300378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
302889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
303713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
303734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.68ms 
303737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
303737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.9ns 
303738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
306253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
307073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
307099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.71ms 
307100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
307100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
307101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
309601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
310420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
310445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.6ms 
310446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
310446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
310447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
312945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
313765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
313773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.68ms 
313774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
313774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
313775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
316270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
317090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
317108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.87ms 
317109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
317109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
317110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
319623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
320419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
320423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
320424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
320424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
320425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
322943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
323741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
323744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577.4ns 
323745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
323745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
323746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
326260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
327080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
327082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 777.9ns 
327083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
327083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
327084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
329589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
330409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
330416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
330418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
330418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
330418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
332926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
333752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
333758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms 
333760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
333760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
333761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
336265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
337089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
337102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.68ms 
337103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
337103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
337104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
339617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
340444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
340448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
340449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
340449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
340449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
342951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
343772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
343774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 525.4ns 
343775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
343775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
343776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
346279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
347107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
347115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
347117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
347117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.7ns 
347118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
349647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
350444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
350446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 678.7ns 
350448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
350448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
350448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
352981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
353781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
353783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584ns 
353784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
353785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
353785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
356309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
357108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
357114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
357116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
357116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
357116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
359636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
360459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
360463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
360464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
360464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
360465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
362964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
363789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
363798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.08ms 
363800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
363800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
363800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
366308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
367131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
367134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
367136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
367136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
367136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
369644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
370469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
370476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.07ms 
370477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
370477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
370477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
372971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
373796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
373800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
373801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
373801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
373802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
376298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
377120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
377136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.31ms 
377137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
377137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
377138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
379631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
380453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
380457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
380458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
380458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
380459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
382979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
383781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
383784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
383786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
383786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
383786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
386300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
387100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
387104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
387105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
387105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
387106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
389621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
390444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
390461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.58ms 
390462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
390463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
390463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
392958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
393781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
393786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.3ns 
393787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
393787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
393788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
396278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
397100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
397140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.34ms 
397142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
397142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
397143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
399641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
400466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
400469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
400470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
400470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
400471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
402961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
403790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
403812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.14ms 
403814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
403817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.1ms 
403818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
406318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
407147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
407170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.34ms 
407172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
407172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
407173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
409672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
410498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
410522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.11ms 
410523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
410523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
410524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
413045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
413846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
413848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.9ns 
413849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
413850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
413850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
416362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
417163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
417169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
417170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
417170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
417171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
419693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
420520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
420522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
420524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
420524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
420524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
423025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
423852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
423855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 790.21ns 
423856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
423856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
423857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
426355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
427183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
427185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 876.91ns 
427186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
427186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
427187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
429683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
430514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
430517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
430519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
430519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
430519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
433014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
433846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
433849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
433850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
433851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.2ns 
433851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
436364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
437171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
437180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.49ms 
437182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
437182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
437183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
439701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
440535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
440547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.67ms 
440549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
440549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
440549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
443054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
443881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
443893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.66ms 
443894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
443894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
443895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
446392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
447226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
447237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.93ms 
447239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
447239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
447239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
449736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
450573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
450578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
450580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
450580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.4ns 
450581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
453091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
453907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
453913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
453914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
453914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
453915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
456440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
457274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
457276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 675.91ns 
457277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
457277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
457278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
459778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
460613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
460615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
460617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
460617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
460617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
463117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
463951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
463953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 852.41ns 
463955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
463955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
463955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
466475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
467287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
467298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.27ms 
467299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
467300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
467300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
469821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
470656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
470660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
470661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
470661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
470661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
473154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
473993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
474001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
474003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
474003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.6ns 
474004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
476504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
477337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
477340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 676ns 
477341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
477341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
477341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
479854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
480664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
480666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.21ns 
480667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
480668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
480668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
483192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
484033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
484037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
484038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
484038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
484039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
486529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
487367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
487369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
487370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
487370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
487371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
489885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
490695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
490700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
490701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
490702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
490702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
493214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
494047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
494049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
494051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
494051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
494051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
496541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
497375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
497380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
497381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
497381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
497382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
499900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
500709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
500712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
500713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
500713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
500714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
503234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
504066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
504077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.81ms 
504078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
504079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
504079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
506573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
507405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
507407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 861.51ns 
507408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
507408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
507409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
509917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
510751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
510757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
510759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
510759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
510759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
513260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
514094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
514096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 889.71ns 
514098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
514098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
514098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
516612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
517424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
517426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840.4ns 
517427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
517427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
517428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
519951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
520784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
520789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
520790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
520794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.68ms 
520795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
523285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
524120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
524123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
524124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
524124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
524125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
526646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
527482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
527485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
527486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
527486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
527487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
529985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
530825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
530829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
530830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
530830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
530831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
533343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
534176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
534181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
534183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
534183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
534184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
536691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
537529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
537544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.82ms 
537545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
537545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
537546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
540084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
540901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
540945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.7ms 
540946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
540947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
540947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
543448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
544283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
544294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.81ms 
544296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
544296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
544296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
546808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
547620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
547658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.13ms 
547660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
547660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.7ns 
547661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
550155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
550995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
551021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.14ms 
551022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
551022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
551023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
553539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
554372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
554398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.48ms 
554399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
554399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
554400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
556918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
557754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
557778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.08ms 
557780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
557780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
557780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
560301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
561138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
561153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.91ms 
561155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
561155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
561155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
563657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
564492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
564524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.22ms 
564525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
564525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
564526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
567043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
567877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
567926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.89ms 
567927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
567927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
567928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
570446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
571258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
571306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.32ms 
571308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
571308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.1ns 
571309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
573832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
574667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
574710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.71ms 
574711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
574712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
574712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
577226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
578062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
578106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.63ms 
578108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
578108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
578109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
580602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
581437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
581562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.35ms 
581564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
581565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.8ns 
581565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
584102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
584940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
584948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.16ms 
584949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
584949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
584950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
587467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
588303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
588310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
588311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
588312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
588312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
590816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
591655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
591660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
591661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
591661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
591662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
594179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
595014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
595032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.47ms 
595034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
595034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
595034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
597548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
598384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
598396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.54ms 
598398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
598398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
598398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
600894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
601732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
601735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
601736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
601736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
601737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
604251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
605087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
605104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.86ms 
605106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
605106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
605106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
607620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
608455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
608471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.94ms 
608473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
608473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
608473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
610996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
611814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
611833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.31ms 
611834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
611835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
611835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
614345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
615180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
615183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
615184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
615184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
615185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
617692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
618526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
618530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
618531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
618531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
618532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
621038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
621876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
621882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
621883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
621883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
621884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
624401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
625216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
625222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
625223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
625223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
625224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
627732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
628567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
628634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.81ms 
628635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
628635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
628636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
631159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
631996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
632022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.87ms 
632023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
632023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
632024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
634533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
635367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
635389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.59ms 
635390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
635390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
635390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
637902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
638740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
638742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 292.8ns 
638743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
638743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
638744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
641254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
642089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
642285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 184.69ms 
642288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
642288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.5ns 
642289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
644808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
645647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
645697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.32ms 
645698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
645698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
645699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
648221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
649036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
649038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 334.5ns 
649040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
649040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
649040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
651563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
652399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
652400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 353.4ns 
652402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
652402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
652402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
654908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
655744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
655746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 344.7ns 
655747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
655747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 575.5ns 
655748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
658255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
659090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
659091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 467.8ns 
659093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
659093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
659093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
661598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
662434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
662527     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
662544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.05ms 
662547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
662547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204ns 
662548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
665073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
665911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
665960     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
665961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.33ms 
665962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
665962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
665963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
668494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
669342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
669343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 
669373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
669415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
669436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
669444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
669454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
669456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
669457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
669460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
669465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
669467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
669471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
669472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
669686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
669688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
669689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
669691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
669692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
669828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
669830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
669833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
669835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
669836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
669837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
669997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
669999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
670000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
670001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
670007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
670010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
670118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
670120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
670121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
670122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
670123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
670124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
670137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
670138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
670138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
670141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
670142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
670143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
670151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
670152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
670154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
670154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
670155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
670157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
670262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
670263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
670264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
670378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
670379     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)'' 
670381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
670382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
670383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
670384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
670385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
670385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
670388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
670390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
670391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
670391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
670392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
670478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
670480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
670482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
670482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
670483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
670484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
670484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
670583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
670584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
670585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
670586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
670587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
670587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
670588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
670589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
670664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
670665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
670737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
670741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
670744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
670745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
670746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
670748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
670748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
670749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
670750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
670751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
670757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
670761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
670839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
670840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
670841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
670842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
670843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
670843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
670844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
670845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
670889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
670894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
670977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
670979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
670981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
670982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
670983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
670984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
671100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
671103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
671105     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)'' 
671106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
671107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
671108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
671109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
671110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
671117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
671118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
671120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
671120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
671239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
671240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
671241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
671242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
671242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
671243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
671334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
671335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
671336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
671337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
671338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
671339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
671339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
671340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
671415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
671416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
671485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
671486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
671487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
671491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
671494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
671498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
671608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
671614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
671615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
671616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
671625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
671703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
675014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
675015     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)'' 
675021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
675021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
675022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
675023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
675024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
675031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
675033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
675034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
675034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
675035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
675127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
675131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
675132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
675133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
675133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
675134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
675135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
675230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
675231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
675232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
675234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
675234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
675235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
675235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
675279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
675354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
675355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
675433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
675437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
675441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
675442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
675443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
675444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
675454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
675542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
675543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
675544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
675545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
675615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
675623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
675624     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)'' 
675626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
675627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
675628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
675628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
675629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
675639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
675640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
675642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
675642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
675646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
675733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
675735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
675736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
675737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
675738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
675825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
675830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
675831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
675832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
675832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
675833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
675834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
675928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
675930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
675931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
675932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
675933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
675934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
675934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
675935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
675936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
675937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
675938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
675939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
675939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
675940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
675941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
676024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
676025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
676031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
676105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
676183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
676184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
676185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
676186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
676187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
676188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
676188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
676189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
676190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
676272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
676277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
676366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
676368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
676369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
676370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
676370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
676371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
676371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
676372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
676377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
676378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
676454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
676459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
676464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
676560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
676561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
676561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
676562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
676563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
676563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
676563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
676564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
676616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
676617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
676617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
676618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
676619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
676624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
676628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
676742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
676826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
676828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
676828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
676829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
676990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
677125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
677126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
680002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
680007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
680008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
680009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
680010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
680122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
680123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
680124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
680125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
680126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
680229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
683093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
686151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
686156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
686157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
686157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
686158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
686270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
686272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
686273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
686274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
686275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
687341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
687341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.3ns 
687342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
689959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
690812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
690814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
690814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
690822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
690834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
690836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
690838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
690839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
690843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
690844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
690847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
690850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
690851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
690859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
690861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
690861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
690903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
690904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
690904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
690905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
690905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
690962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
690962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
690963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
690964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
690965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
690968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
690968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
690968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
690969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
690970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
690971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
691043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
691043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
691044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
691045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
691045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
691046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
691124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
691124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
691125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
691125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
691126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
691127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
691127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
691127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
691128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
691129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
691129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
691129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
691130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
691130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
691131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
691131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
691131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
691132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
691133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
691135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
691170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
691171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
691225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
691226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
691227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
691229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
691229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
691230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
691276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
691278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
691279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
691280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
691281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
691282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
691282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
691325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
691328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
691330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
691379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
691429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
691429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
691430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
694008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
694902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
694934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.93ms