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

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
198
tests
failures
ignored
12m51.43s
duration
100%
successful
Tests
Standard output
Tests

Test	Method name	Duration	Result
powPositive	data()[100]	3.682s	passed
powPositiveConcrete	data()[101]	3.698s	passed
powGeq1Concrete	data()[102]	3.747s	passed
pow2InIntLower	data()[103]	3.724s	passed
pow2InIntUpper	data()[104]	3.699s	passed
logSelfConcrete	data()[105]	3.737s	passed
log1Concrete	data()[106]	3.675s	passed
logProduct	data()[107]	3.746s	passed
logTimesBaseConcrete	data()[108]	3.784s	passed
logProdIdentity	data()[109]	3.751s	passed
moduloByteIsInByte	data()[10]	3.987s	passed
logProdIdentityConcrete	data()[110]	3.729s	passed
logPowIdentity	data()[111]	3.700s	passed
logPowIdentityConcrete	data()[112]	3.804s	passed
logPositive	data()[113]	3.747s	passed
logPositiveConcrete	data()[114]	3.720s	passed
logMono	data()[115]	3.896s	passed
logMonoConcrete	data()[116]	3.710s	passed
powLogLess	data()[117]	3.762s	passed
powLogMore2	data()[118]	3.781s	passed
logLessThanPow	data()[119]	3.813s	passed
moduloCharIsInChar	data()[11]	3.803s	passed
logLessThanPowConcrete	data()[120]	3.816s	passed
logSqueeze	data()[121]	3.764s	passed
ifthenelse_equals	data()[122]	3.692s	passed
ifthenelse_equals_1	data()[123]	3.695s	passed
ifthenelse_equals_2	data()[124]	3.786s	passed
disjointWithSingleton1	data()[125]	3.734s	passed
disjointWithSingleton2	data()[126]	3.717s	passed
disjointArrayRanges	data()[127]	3.750s	passed
disjointArrayRangeAllFields1	data()[128]	3.745s	passed
disjointArrayRangeAllFields2	data()[129]	3.697s	passed
div_unique1	data()[12]	3.899s	passed
seqSelfDefinition	data()[130]	3.739s	passed
seqOutsideValue	data()[131]	3.730s	passed
castedGetAny	data()[132]	3.741s	passed
seqGetAlphaCast	data()[133]	3.696s	passed
getOfSeqSingleton	data()[134]	3.740s	passed
getOfSeqSingletonConcrete	data()[135]	3.803s	passed
getOfSeqConcat	data()[136]	3.728s	passed
getOfSeqSub	data()[137]	3.742s	passed
getOfSeqReverse	data()[138]	3.681s	passed
lenOfSeqEmpty	data()[139]	3.744s	passed
div_unique2	data()[13]	3.990s	passed
lenOfSeqSingleton	data()[140]	3.783s	passed
lenOfSeqConcat	data()[141]	3.782s	passed
lenOfSeqSub	data()[142]	3.732s	passed
lenOfSeqReverse	data()[143]	3.702s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.769s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.733s	passed
getOfSeqSingletonEQ	data()[146]	3.743s	passed
getOfSeqConcatEQ	data()[147]	3.784s	passed
getOfSeqSubEQ	data()[148]	3.780s	passed
getOfSeqReverseEQ	data()[149]	3.803s	passed
div_exists	data()[14]	4.107s	passed
lenOfSeqEmptyEQ	data()[150]	3.843s	passed
lenOfSeqSingletonEQ	data()[151]	3.908s	passed
lenOfSeqConcatEQ	data()[152]	3.834s	passed
lenOfSeqSubEQ	data()[153]	3.705s	passed
lenOfSeqReverseEQ	data()[154]	3.681s	passed
getOfSeqDefEQ	data()[155]	3.706s	passed
lenOfSeqDefEQ	data()[156]	3.795s	passed
seqConcatWithSeqEmpty1	data()[157]	3.709s	passed
seqConcatWithSeqEmpty2	data()[158]	3.736s	passed
seqReverseOfSeqEmpty	data()[159]	3.755s	passed
div_one	data()[15]	3.732s	passed
subSeqComplete	data()[160]	3.717s	passed
subSeqTailR	data()[161]	3.733s	passed
subSeqTailL	data()[162]	3.716s	passed
subSeqTailEQR	data()[163]	3.696s	passed
subSeqTailEQL	data()[164]	3.836s	passed
seqDef_split	data()[165]	3.720s	passed
seqDef_induction_upper	data()[166]	3.822s	passed
seqDef_induction_upper_concrete	data()[167]	3.845s	passed
seqDef_induction_lower	data()[168]	3.807s	passed
seqDef_induction_lower_concrete	data()[169]	3.787s	passed
jdiv_one	data()[16]	3.855s	passed
seqDef_split_in_three	data()[170]	3.841s	passed
seqDef_empty	data()[171]	3.751s	passed
seqDef_one_summand	data()[172]	3.772s	passed
seqDef_lower_equals_upper	data()[173]	3.724s	passed
seqDefOfSeq	data()[174]	3.730s	passed
seqSelfDefinitionEQ2	data()[175]	3.780s	passed
indexOfSeqSingleton	data()[176]	3.795s	passed
indexOfSeqConcatFirst	data()[177]	3.776s	passed
indexOfSeqConcatSecond	data()[178]	3.696s	passed
indexOfSeqSub	data()[179]	3.706s	passed
div_zero	data()[17]	3.870s	passed
lenOfArray2seq	data()[180]	3.716s	passed
getAnyOfArray2seq	data()[181]	3.701s	passed
getOfArray2seq	data()[182]	3.678s	passed
getAnyOfNPermInv	data()[183]	3.699s	passed
seqNPermRange	data()[184]	3.754s	passed
seqPermTrans	data()[185]	3.773s	passed
seqPermRefl	data()[186]	3.736s	passed
seqPermSplit	data()[187]	3.674s	passed
seqNPermRight	data()[188]	3.854s	passed
seqPermFromSwap	data()[189]	3.741s	passed
divResZero1	data()[18]	3.767s	passed
seqPermTransAlt0	data()[190]	3.704s	passed
seqPermTransAlt1	data()[191]	3.796s	passed
seqPermTransAlt2	data()[192]	3.698s	passed
seqPermTransAlt3	data()[193]	3.728s	passed
seqPermForall	data()[194]	3.852s	passed
seqPermExists	data()[195]	3.837s	passed
schiffl_lemma_2	data()[196]	25.735s	passed
schiffl_thm_1	data()[197]	4.657s	passed
eqSameSeq	data()[198]	4.082s	passed
divResZero2	data()[19]	3.814s	passed
eqTermCut	data()[1]	4.693s	passed
divResOne1	data()[20]	3.794s	passed
divResOne2	data()[21]	3.770s	passed
div_cancel1	data()[22]	3.784s	passed
div_cancel2	data()[23]	3.712s	passed
divAddMultDenom	data()[24]	3.763s	passed
divMinus	data()[25]	3.792s	passed
divMinusDenom	data()[26]	3.820s	passed
divLeastDPos	data()[27]	3.683s	passed
divLeastDNeg	data()[28]	3.754s	passed
divGreatestDPos	data()[29]	3.836s	passed
equivAllRight	data()[2]	4.223s	passed
divGreatestDNeg	data()[30]	3.759s	passed
divIncreasingPos	data()[31]	3.868s	passed
divIncreasingNeg	data()[32]	3.820s	passed
jdiv_zero	data()[33]	3.732s	passed
jdivPulloutMinusNum	data()[34]	3.680s	passed
jdivPulloutMinusDenom	data()[35]	3.882s	passed
jdiv_uniquePosPos	data()[36]	3.876s	passed
jdiv_uniquePosNeg	data()[37]	3.838s	passed
jdiv_uniqueNegPos	data()[38]	3.694s	passed
jdiv_uniqueNegNeg	data()[39]	3.736s	passed
irrflConcrete1	data()[3]	4.225s	passed
jdivMultDenom1	data()[40]	3.788s	passed
jdivMultDenom2	data()[41]	3.774s	passed
mod_geZero	data()[42]	3.667s	passed
mod_lessDenom	data()[43]	3.698s	passed
jmod_NumPos	data()[44]	3.759s	passed
jmod_NumNeg	data()[45]	3.852s	passed
jmod_geZero	data()[46]	3.708s	passed
jmodNumZero	data()[47]	3.698s	passed
jmod_pulloutminusNum	data()[48]	3.819s	passed
jmod_pulloutminusDenom	data()[49]	3.671s	passed
irrflConcrete2	data()[4]	3.969s	passed
jmodUnique1	data()[50]	3.862s	passed
jmodUnique2	data()[51]	3.794s	passed
intDivRem	data()[52]	3.741s	passed
jmodjmod	data()[53]	3.723s	passed
jmodDivisible	data()[54]	3.788s	passed
jmodDivisibleRep	data()[55]	3.695s	passed
jdivAddMultDenom	data()[56]	3.949s	passed
jmodAltZero	data()[57]	3.743s	passed
jmodAddMultDenomZero	data()[58]	3.748s	passed
polyDiv_zero	data()[59]	3.764s	passed
cancel_gtPos	data()[5]	4.075s	passed
polyMod_ltdivDenom	data()[60]	3.833s	passed
bsum_empty	data()[61]	3.739s	passed
bsum_induction_upper	data()[62]	3.681s	passed
bsum_induction_lower	data()[63]	3.740s	passed
bsum_num_of_bounds	data()[64]	3.765s	passed
bsum_num_of_bounds2	data()[65]	3.759s	passed
bsum_induction_upper2	data()[66]	3.664s	passed
bsum_induction_upper_concrete	data()[67]	3.696s	passed
bsum_induction_upper_concrete_2	data()[68]	3.667s	passed
bsum_induction_upper2_concrete	data()[69]	3.752s	passed
cancel_gtNeg	data()[6]	3.971s	passed
bsum_induction_lower_concrete	data()[70]	3.700s	passed
bsum_induction_lower2	data()[71]	3.718s	passed
bsum_induction_lower2_concrete	data()[72]	3.754s	passed
bsum_positive	data()[73]	3.769s	passed
bsum_upper_bound	data()[74]	3.724s	passed
bsum_lower_bound	data()[75]	3.753s	passed
bsum_positive_lower_bound_element	data()[76]	3.864s	passed
bsum_sub_same_index	data()[77]	3.741s	passed
bsum_less_same_index	data()[78]	3.799s	passed
bsum_equal_except_one_index	data()[79]	3.744s	passed
moduloIntIsInInt	data()[7]	4.103s	passed
bsum_num_of_is_max	data()[80]	3.750s	passed
bsum_num_of_is_max2	data()[81]	3.713s	passed
bsum_num_of_is_max3	data()[82]	3.733s	passed
bsum_num_of_is_max4	data()[83]	3.716s	passed
bsum_num_of_lt_max	data()[84]	3.850s	passed
bsum_num_of_lt_max2	data()[85]	3.875s	passed
bsum_num_of_lt_max3	data()[86]	3.845s	passed
bsum_num_of_lt_max4	data()[87]	3.808s	passed
bsum_num_of_gt0	data()[88]	3.814s	passed
bsum_num_of_gt0_alt	data()[89]	3.721s	passed
moduloLongIsInLong	data()[8]	3.878s	passed
bsum_add_concrete	data()[90]	3.780s	passed
bprod_all_positive	data()[91]	3.760s	passed
bprod_split	data()[92]	3.786s	passed
powConcrete0	data()[93]	3.728s	passed
powConcrete1	data()[94]	3.720s	passed
powSplitFactor	data()[95]	3.683s	passed
powAdd	data()[96]	3.789s	passed
powMono	data()[97]	3.712s	passed
powMonoConcrete	data()[98]	3.750s	passed
powMonoConcreteRight	data()[99]	3.729s	passed
moduloShortIsInShort	data()[9]	3.922s	passed
Standard output

817        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
846        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 13.44ms 
1149       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1180       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)

2364       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2400       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2403       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2403       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4644       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10802      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.65s 
10897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10949      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.5ns 
10968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10969      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.6ns 
10975      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14566      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
14569      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15623      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15650      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.95ms 
15664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.1ns 
15666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18842      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
18842      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
19871      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19885      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.42ms 
19888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19888      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.7ns 
19896      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23073      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
23073      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24111      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
24114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24115      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 874.31ns 
24116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27089      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
27090      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
28074      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
28080      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
28084      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
28085      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 534.81ns 
28086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31147      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
31148      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
32104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
32156      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.57ms 
32163      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
32164      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.61ms 
32166      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
35138      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
36107      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
36129      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.75ms 
36138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
36138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.71ns 
36139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39203      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
39204      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
40229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
40233      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 944.31ns 
40236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
40237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.5ns 
40238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43149      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
43150      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
44109      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
44112      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.51ns 
44115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
44115      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.9ns 
44116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
47093      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
48032      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
48034      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.76ns 
48037      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
48037      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.68ns 
48038      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51021      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
51021      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
52013      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
52019      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
52024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
52024      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.4ns 
52026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54902      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
54903      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
55822      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
55825      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 714.11ns 
55828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
55828      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.9ns 
55830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58739      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
58739      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
59676      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
59724      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.96ms 
59727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
59728      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
59729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62686      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
62686      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
63615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
63710      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.27ms 
63719      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
63720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 640.31ns 
63721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66640      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
66640      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
67616      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
67822      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 188.87ms 
67826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
67826      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.7ns 
67828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70646      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
70647      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
71547      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
71555      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.41ms 
71557      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
71557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.4ns 
71558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
74480      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
75406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
75410      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
75413      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
75414      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.4ns 
75415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
78296      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
79229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
79281      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.38ms 
79283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
79284      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.6ns 
79285      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82106      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
82106      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
83026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
83048      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.65ms 
83050      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
83050      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns 
83051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85888      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
85889      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
86846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
86862      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.26ms 
86864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
86865      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387ns 
86866      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
89720      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
90635      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
90656      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.07ms 
90658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
90658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351ns 
90660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93497      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
93497      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
94407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
94427      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.64ms 
94428      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
94428      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
94429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97267      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
97267      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
98184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
98210      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.82ms 
98213      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
98213      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.6ns 
98214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
101002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
101920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
101924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
101925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
101925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.7ns 
101927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
104742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
105641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
105686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.8ms 
105688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
105688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
105689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
108504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
109412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
109477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.31ms 
109480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
109481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.4ns 
109482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
112315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
113244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
113298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.26ms 
113309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
113310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 968.51ns 
113312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
116081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
116979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
116989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.55ms 
116991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
116991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.2ns 
116992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
119843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
120728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
120743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms 
120745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
120745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.4ns 
120746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
123629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
124563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
124578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.84ms 
124582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
124582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340ns 
124583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
127424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
128328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
128338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 
128340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
128340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
128341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
131231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
132197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
132206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.93ms 
132208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
132208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
132209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
135113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
136018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
136027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.56ms 
136028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
136028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
136029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
138810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
139753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
139758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
139759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
139760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
139761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
142506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
143427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
143438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.69ms 
143440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
143440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.1ns 
143441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
146330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
147253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
147320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.51ms 
147323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
147337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 14.11ms 
147338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
150198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
151164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
151197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.14ms 
151200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
151201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.21ms 
151203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
154075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
155014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
155035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.64ms 
155036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
155036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.9ns 
155037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
157812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
158708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
158729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.68ms 
158731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
158731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
158732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
161529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
162446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
162465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.07ms 
162467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
162467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
162468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
165303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
166209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
166253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.06ms 
166254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
166255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
166255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
169126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
170022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
170028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
170029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
170029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.51ns 
170030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
172768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
173690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
173694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
173695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
173696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
173696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
176495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
177384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
177392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.31ms 
177394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
177394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
177394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
180218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
181141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
181151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.76ms 
181153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
181153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
181154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
184079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
184982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
185003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.02ms 
185004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
185004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
185005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
187785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
188703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
188711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.18ms 
188712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
188713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
188713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
191503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
192403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
192406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
192412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
192412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.51ns 
192413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
195315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
196224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
196229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
196230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
196230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.31ns 
196231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
199012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
199892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
199899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
199901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
199901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.7ns 
199903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
202764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
203664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
203760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.74ms 
203764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
203764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
203765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
206570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
207467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
207556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.69ms 
207557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
207557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
207558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
210377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
211294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
211297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
211299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
211299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
211300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
214093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
214983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
215020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.92ms 
215022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
215022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.91ns 
215023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
217857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
218765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
218808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.44ms 
218811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
218811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.31ns 
218812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
221601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
222500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
222503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
222505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
222505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
222506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
225376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
226304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
226452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 128.76ms 
226455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
226455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.21ns 
226456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
229284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
230185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
230196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 
230197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
230197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
230198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
233024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
233936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
233944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ms 
233945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
233945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
233946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
236799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
237689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
237707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.93ms 
237708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
237708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
237709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
240541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
241525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
241540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.69ms 
241542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
241542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
241543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
244342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
245275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
245278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
245280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
245280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
245281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
248059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
248956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
248961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
248964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
248964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
248965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
251769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
252684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
252703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.55ms 
252704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
252704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
252705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
255530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
256453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
256467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.69ms 
256469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
256469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
256470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
259295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
260211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
260226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.72ms 
260228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
260228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.5ns 
260229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
263022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
263887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
263891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
263892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
263892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
263893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
266662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
267582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
267586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
267588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
267588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.01ns 
267589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
270367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
271248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
271253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
271254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
271254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
271255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
274090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
275002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
275005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
275007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
275008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.31ns 
275009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
277770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
278703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
278705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 592.71ns 
278706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
278706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
278707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
281504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
282420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
282424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
282425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
282425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
282426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
285254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
286173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
286176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 863.42ns 
286179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
286179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
286180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
288968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
289886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
289944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.34ms 
289948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
289948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.5ns 
289949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
292723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
293633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
293670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.58ms 
293671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
293672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
293672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
296489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
297385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
297423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.04ms 
297426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
297426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
297427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
300247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
301232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
301287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.47ms 
301289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
301289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.2ns 
301290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
304108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
304998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
305028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.56ms 
305030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
305030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
305031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
307831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
308749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
308826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.29ms 
308829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
308830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.21ns 
308831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
311636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
312543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
312571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.9ms 
312572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
312573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
312573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
315380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
316301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
316322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.16ms 
316323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
316323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
316324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
319110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
320014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
320035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.79ms 
320036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
320036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
320037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
322825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
323749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
323767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.43ms 
323768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
323768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
323769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
326582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
327460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
327484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.51ms 
327485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
327485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
327486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
330391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
331310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
331334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.92ms 
331335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
331335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
331336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
334262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
335182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
335207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.84ms 
335209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
335209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
335211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
338116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
339030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
339053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.85ms 
339054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
339055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
339055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
341951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
342839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
342861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.11ms 
342863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
342863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
342864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
345730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
346656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
346675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.35ms 
346677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
346677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.5ns 
346678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
349453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
350375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
350396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.17ms 
350397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
350397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
350398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
353239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
354170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
354177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
354178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
354178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
354179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
357015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
357922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
357936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.52ms 
357938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
357938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
357939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
360743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
361718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
361722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
361723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
361723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
361724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
364532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
365448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
365450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 603.91ns 
365452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
365452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
365453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
368256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
369168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
369170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 814.41ns 
369172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
369172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
369172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
371921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
372846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
372854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
372855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
372855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
372856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
375687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
376636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
376642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
376644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
376644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.9ns 
376646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
379431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
380342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
380354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
380355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
380356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
380356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
383175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
384101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
384104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
384106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
384106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
384107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
386916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
387831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
387833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 506.81ns 
387834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
387835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
387835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
390639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
391509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
391515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
391516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
391517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
391517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
394288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
395211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
395214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 685.91ns 
395215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
395215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
395216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
398066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
398958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
398960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.81ns 
398961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
398961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
398962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
401779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
402683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
402685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 593.91ns 
402686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
402686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
402687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
405458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
406379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
406383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
406384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
406385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
406385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
409187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
410112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
410120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
410121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
410121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
410122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
412915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
413791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
413795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
413796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
413796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
413797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
416583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
417530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
417541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.96ms 
417543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
417543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.7ns 
417544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
420366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
421321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
421326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
421327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
421327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
421328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
424156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
425061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
425076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.36ms 
425077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
425077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
425078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
427862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
428802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
428805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
428807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
428807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.3ns 
428808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
431604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
432501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
432505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
432506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
432506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
432507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
435383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
436305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
436309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
436310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
436310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
436311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
439128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
440036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
440056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.42ms 
440058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
440058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
440059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
442856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
443770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
443775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 539.71ns 
443777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
443777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
443778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
446710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
447637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
447672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.99ms 
447674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
447674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
447675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
450457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
451379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
451382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
451384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
451384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
451385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
454218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
455123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
455144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.28ms 
455146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
455147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.7ns 
455148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
457988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
458905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
458926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.02ms 
458927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
458927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
458928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
461827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
462715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
462739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.6ms 
462740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
462740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
462741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
465645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
466551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
466554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 645.8ns 
466555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
466555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
466556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
469393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
470313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
470318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
470319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
470320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
470320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
473133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
474008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
474011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
474012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
474012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
474013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
476789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
477703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
477705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 877.11ns 
477707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
477707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
477707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
480533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
481489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
481491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.41ns 
481492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
481493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
481493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
484297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
485222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
485226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
485227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
485227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
485228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
488028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
488939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
488942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
488944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
488944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
488945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
491772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
492682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
492692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.44ms 
492693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
492693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
492694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
495510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
496423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
496431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.76ms 
496439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
496439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
496440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
499211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
500126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
500134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
500136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
500136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
500136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
502949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
503857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
503873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.95ms 
503874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
503875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns 
503875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
506669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
507599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
507603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
507604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
507605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
507605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
510409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
511339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
511344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
511346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
511346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
511346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
514124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
515038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
515040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 791.01ns 
515042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
515042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
515043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
517845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
518778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
518781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
518782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
518782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
518783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
521616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
522581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
522584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
522585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
522585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
522586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
525362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
526300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
526311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.24ms 
526313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
526314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.7ns 
526318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
529143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
530050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
530053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
530054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
530054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
530055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
532809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
533728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
533734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
533736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
533736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
533736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
536500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
537476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
537478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 820.91ns 
537480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
537480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
537480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
540316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
541259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
541262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 724.71ns 
541263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
541263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
541264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
544083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
545039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
545043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
545045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
545045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.2ns 
545046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
547872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
548773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
548775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 887.61ns 
548777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
548777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
548777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
551542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
552474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
552477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
552478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
552478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
552479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
555300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
556244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
556247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
556248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
556248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
556249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
559049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
559973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
559979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 
559981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
559981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
559982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
562810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
563720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
563723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 946.71ns 
563724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
563724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
563725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
566527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
567493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
567506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.05ms 
567507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
567507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
567508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
570358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
571284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
571286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.11ns 
571287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
571287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
571288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
574152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
575083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
575089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms 
575091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
575091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
575092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
577950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
578929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
578932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
578933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
578933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
578934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
581844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
582838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
582841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 917.61ns 
582842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
582842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
582843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
585768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
586671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
586675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
586676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
586676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
586677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
589442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
590377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
590380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
590381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
590381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
590382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
593142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
594057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
594060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
594062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
594062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
594062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
596848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
597763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
597766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
597767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
597767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
597768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
600564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
601558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
601562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
601563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
601563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
601564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
604356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
605261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
605270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.35ms 
605271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
605271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
605272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
608089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
608997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
609006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.83ms 
609007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
609007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
609008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
611812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
612755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
612762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
612764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
612764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
612765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
615551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
616472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
616479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
616481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
616481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
616481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
619264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
620201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
620213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.67ms 
620214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
620214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
620215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
622992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
623917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
623929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.83ms 
623930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
623930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
623931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
626689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
627610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
627625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.95ms 
627626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
627626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
627627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
630519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
631452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
631460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
631461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
631461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
631462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
634229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
635155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
635180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.54ms 
635182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
635182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
635182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
638054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
638973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
639002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.65ms 
639004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
639004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
639004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
641892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
642819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
642847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.29ms 
642848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
642849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
642849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
645696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
646632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
646654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.71ms 
646656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
646656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
646677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
649490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
650415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
650441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.43ms 
650443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
650443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
650444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
653254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
654226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
654282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.75ms 
654284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
654284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
654285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
657103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
658027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
658033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
658034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
658034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
658035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
660818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
661799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
661806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
661807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
661807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
661808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
664617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
665526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
665529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
665530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
665531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
665531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
668317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
669244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
669259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.61ms 
669261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
669261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
669261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
672090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
673031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
673039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
673041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
673041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.3ns 
673042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
675860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
676831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
676834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
676836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
676836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
676837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
679655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
680599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
680610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.13ms 
680612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
680612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
680613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
683365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
684295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
684306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.68ms 
684308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
684308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
684308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
687040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
687996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
688012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ms 
688014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
688014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
688014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
690793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
691726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
691729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
691730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
691730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
691730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
694480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
695426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
695430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
695431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
695431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
695432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
698189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
699101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
699108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
699109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
699109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
699110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
701881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
702801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
702807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
702808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
702808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
702809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
705553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
706508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
706561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.18ms 
706562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
706562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.2ns 
706563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
709397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
710307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
710333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.04ms 
710335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
710335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 
710336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
713113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
714057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
714070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.62ms 
714071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
714071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
714072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
716786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
717741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
717743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 244.1ns 
717745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
717745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
717746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
720513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
721482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
721597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.31ms 
721599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
721599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.1ns 
721600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
724388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
725294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
725339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.36ms 
725340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
725340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
725341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
728091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
729040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
729042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 189.51ns 
729044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
729044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.11ns 
729045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
731894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
732836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
732838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 231.51ns 
732839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
732839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
732840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
735608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
736535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
736537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 218.81ns 
736538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
736538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
736539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
739315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
740262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
740264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 401.81ns 
740265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
740265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
740266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
743064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
743988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
744106     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
744116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 125.7ms 
744119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
744119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.01ns 
744120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
746971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
747904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
747953     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
747954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.05ms 
747955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
747955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
747956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
750870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
751794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
751796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
751829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
751868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
751883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
751888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
751899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
751900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
751904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
751905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
751910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
751911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
751914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
751916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
752119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
752121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
752122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
752123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
752125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
752280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
752281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
752284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
752285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
752287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
752288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
752496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
752499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
752500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
752501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
752503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
752507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
752662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
752663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
752665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
752666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
752667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
752668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
752676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
752677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
752678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
752680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
752682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
752684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
752693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
752694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
752695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
752696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
752696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
752698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
752834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
752836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
752838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
752972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
752974     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)'' 
752976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
752978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
752979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
752980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
752981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
752984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
752988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
752990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
752992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
752993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
752994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
753117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
753123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
753124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
753126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
753126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
753127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
753129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
753272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
753273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
753274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
753276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
753277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
753278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
753279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
753281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
753396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
753398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
753502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
753506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
753512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
753513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
753516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
753519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
753520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
753520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
753521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
753522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
753532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
753537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
753658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
753659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
753661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
753663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
753664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
753664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
753665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
753666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
753739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
753746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
753868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
753870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
753871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
753872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
753874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
753875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
754040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
754049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
754053     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)'' 
754054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
754056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
754057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
754058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
754059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
754070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
754072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
754076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
754077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
754234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
754236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
754237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
754238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
754239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
754240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
754356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
754363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
754364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
754366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
754367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
754369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
754370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
754371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
754467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
754468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
754573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
754574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
754575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
754581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
754585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
754593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
754754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
754755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
754756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
754757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
754768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
754873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
758968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
758970     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)'' 
758974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
758976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
758977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
758977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
758978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
758987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
758988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
758989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
758990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
758991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
759100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
759104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
759105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
759106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
759106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
759107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
759108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
759217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
759218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
759219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
759220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
759221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
759221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
759222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
759223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
759309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
759310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
759391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
759396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
759401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
759402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
759403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
759404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
759416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
759506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
759507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
759508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
759509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
759592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
759602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
759603     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)'' 
759604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
759605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
759606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
759606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
759607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
759620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
759620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
759621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
759622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
759623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
759729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
759730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
759731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
759732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
759733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
759849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
759854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
759855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
759855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
759856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
759856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
759857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
759974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
759975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
759976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
759978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
759979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
759979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
759980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
759981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
759982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
759983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
759984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
759984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
759985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
759986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
759986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
760090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
760091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
760099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
760192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
760286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
760287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
760288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
760289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
760290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
760291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
760291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
760292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
760292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
760392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
760400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
760565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
760566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
760567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
760568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
760569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
760569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
760570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
760571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
760577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
760578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
760672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
760678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
760684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
760801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
760802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
760803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
760804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
760805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
760806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
760806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
760807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
760882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
760883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
760885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
760885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
760886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
760893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
760899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
761044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
761147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
761148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
761149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
761150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
761345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
761455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
761456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
764991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
764996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
764997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
764998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
765000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
765146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
765147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
765148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
765149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
765150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
765270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
768680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
772261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
772267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
772268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
772269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
772270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
772400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
772400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
772401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
772402     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)' ...' 
772403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
773689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
773690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.1ns 
773691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
776504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
777492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
777494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
777494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
777500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
777511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
777513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
777516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
777517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
777522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
777522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
777526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
777527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
777529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
777539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
777540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
777542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
777596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
777597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
777598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
777599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
777600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
777685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
777686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
777686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
777687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
777688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
777693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
777693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
777694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
777694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
777696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
777697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
777798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
777799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
777800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
777800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
777802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
777803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
777910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
777911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
777911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
777912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
777913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
777914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
777914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
777915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
777917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
777918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
777918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
777919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
777919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
777920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
777921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
777921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
777922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
777923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
777924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
777927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
777974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
777975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
778045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
778046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
778047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
778048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
778049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
778050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
778122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
778125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
778126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
778127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
778129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
778130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
778131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
778193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
778196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
778200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
778273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
778348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
778348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.71ns 
778349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
781381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
781382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
782407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
782427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ms