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

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
198
tests
failures
ignored
10m0.93s
duration
100%
successful
Tests
Standard output
Tests

Test	Method name	Duration	Result
powPositive	data()[100]	2.899s	passed
powPositiveConcrete	data()[101]	2.898s	passed
powGeq1Concrete	data()[102]	2.902s	passed
pow2InIntLower	data()[103]	2.897s	passed
pow2InIntUpper	data()[104]	2.899s	passed
logSelfConcrete	data()[105]	2.897s	passed
log1Concrete	data()[106]	2.909s	passed
logProduct	data()[107]	2.902s	passed
logTimesBaseConcrete	data()[108]	2.901s	passed
logProdIdentity	data()[109]	2.923s	passed
moduloByteIsInByte	data()[10]	2.952s	passed
logProdIdentityConcrete	data()[110]	2.912s	passed
logPowIdentity	data()[111]	2.881s	passed
logPowIdentityConcrete	data()[112]	2.897s	passed
logPositive	data()[113]	2.904s	passed
logPositiveConcrete	data()[114]	2.899s	passed
logMono	data()[115]	2.923s	passed
logMonoConcrete	data()[116]	2.896s	passed
powLogLess	data()[117]	2.917s	passed
powLogMore2	data()[118]	2.928s	passed
logLessThanPow	data()[119]	2.915s	passed
moduloCharIsInChar	data()[11]	2.974s	passed
logLessThanPowConcrete	data()[120]	2.894s	passed
logSqueeze	data()[121]	2.893s	passed
ifthenelse_equals	data()[122]	2.896s	passed
ifthenelse_equals_1	data()[123]	2.892s	passed
ifthenelse_equals_2	data()[124]	2.906s	passed
disjointWithSingleton1	data()[125]	2.898s	passed
disjointWithSingleton2	data()[126]	2.892s	passed
disjointArrayRanges	data()[127]	2.904s	passed
disjointArrayRangeAllFields1	data()[128]	2.904s	passed
disjointArrayRangeAllFields2	data()[129]	2.902s	passed
div_unique1	data()[12]	3.042s	passed
seqSelfDefinition	data()[130]	2.917s	passed
seqOutsideValue	data()[131]	2.915s	passed
castedGetAny	data()[132]	2.916s	passed
seqGetAlphaCast	data()[133]	2.927s	passed
getOfSeqSingleton	data()[134]	2.910s	passed
getOfSeqSingletonConcrete	data()[135]	2.902s	passed
getOfSeqConcat	data()[136]	2.951s	passed
getOfSeqSub	data()[137]	3.094s	passed
getOfSeqReverse	data()[138]	2.936s	passed
lenOfSeqEmpty	data()[139]	2.905s	passed
div_unique2	data()[13]	3.028s	passed
lenOfSeqSingleton	data()[140]	2.944s	passed
lenOfSeqConcat	data()[141]	2.908s	passed
lenOfSeqSub	data()[142]	2.908s	passed
lenOfSeqReverse	data()[143]	2.900s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	2.951s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	2.948s	passed
getOfSeqSingletonEQ	data()[146]	2.898s	passed
getOfSeqConcatEQ	data()[147]	2.924s	passed
getOfSeqSubEQ	data()[148]	2.901s	passed
getOfSeqReverseEQ	data()[149]	2.901s	passed
div_exists	data()[14]	3.082s	passed
lenOfSeqEmptyEQ	data()[150]	2.897s	passed
lenOfSeqSingletonEQ	data()[151]	2.896s	passed
lenOfSeqConcatEQ	data()[152]	2.899s	passed
lenOfSeqSubEQ	data()[153]	2.920s	passed
lenOfSeqReverseEQ	data()[154]	2.896s	passed
getOfSeqDefEQ	data()[155]	2.894s	passed
lenOfSeqDefEQ	data()[156]	2.895s	passed
seqConcatWithSeqEmpty1	data()[157]	2.929s	passed
seqConcatWithSeqEmpty2	data()[158]	2.916s	passed
seqReverseOfSeqEmpty	data()[159]	2.901s	passed
div_one	data()[15]	2.961s	passed
subSeqComplete	data()[160]	2.905s	passed
subSeqTailR	data()[161]	2.936s	passed
subSeqTailL	data()[162]	2.928s	passed
subSeqTailEQR	data()[163]	2.923s	passed
subSeqTailEQL	data()[164]	2.934s	passed
seqDef_split	data()[165]	2.942s	passed
seqDef_induction_upper	data()[166]	2.953s	passed
seqDef_induction_upper_concrete	data()[167]	2.959s	passed
seqDef_induction_lower	data()[168]	2.951s	passed
seqDef_induction_lower_concrete	data()[169]	2.942s	passed
jdiv_one	data()[16]	2.941s	passed
seqDef_split_in_three	data()[170]	3.031s	passed
seqDef_empty	data()[171]	2.919s	passed
seqDef_one_summand	data()[172]	2.931s	passed
seqDef_lower_equals_upper	data()[173]	2.905s	passed
seqDefOfSeq	data()[174]	2.910s	passed
seqSelfDefinitionEQ2	data()[175]	2.925s	passed
indexOfSeqSingleton	data()[176]	2.903s	passed
indexOfSeqConcatFirst	data()[177]	2.933s	passed
indexOfSeqConcatSecond	data()[178]	2.915s	passed
indexOfSeqSub	data()[179]	2.943s	passed
div_zero	data()[17]	2.961s	passed
lenOfArray2seq	data()[180]	2.898s	passed
getAnyOfArray2seq	data()[181]	2.914s	passed
getOfArray2seq	data()[182]	2.900s	passed
getAnyOfNPermInv	data()[183]	2.924s	passed
seqNPermRange	data()[184]	2.958s	passed
seqPermTrans	data()[185]	2.948s	passed
seqPermRefl	data()[186]	2.924s	passed
seqPermSplit	data()[187]	2.914s	passed
seqNPermRight	data()[188]	3.108s	passed
seqPermFromSwap	data()[189]	2.975s	passed
divResZero1	data()[18]	2.985s	passed
seqPermTransAlt0	data()[190]	2.927s	passed
seqPermTransAlt1	data()[191]	2.902s	passed
seqPermTransAlt2	data()[192]	2.913s	passed
seqPermTransAlt3	data()[193]	2.888s	passed
seqPermForall	data()[194]	3.028s	passed
seqPermExists	data()[195]	3.035s	passed
schiffl_lemma_2	data()[196]	21.519s	passed
schiffl_thm_1	data()[197]	3.658s	passed
eqSameSeq	data()[198]	2.976s	passed
divResZero2	data()[19]	2.939s	passed
eqTermCut	data()[1]	3.499s	passed
divResOne1	data()[20]	2.930s	passed
divResOne2	data()[21]	3.029s	passed
div_cancel1	data()[22]	2.949s	passed
div_cancel2	data()[23]	2.919s	passed
divAddMultDenom	data()[24]	2.965s	passed
divMinus	data()[25]	2.976s	passed
divMinusDenom	data()[26]	2.961s	passed
divLeastDPos	data()[27]	2.921s	passed
divLeastDNeg	data()[28]	2.947s	passed
divGreatestDPos	data()[29]	2.931s	passed
equivAllRight	data()[2]	3.434s	passed
divGreatestDNeg	data()[30]	2.913s	passed
divIncreasingPos	data()[31]	2.938s	passed
divIncreasingNeg	data()[32]	2.915s	passed
jdiv_zero	data()[33]	2.941s	passed
jdivPulloutMinusNum	data()[34]	2.907s	passed
jdivPulloutMinusDenom	data()[35]	2.970s	passed
jdiv_uniquePosPos	data()[36]	2.928s	passed
jdiv_uniquePosNeg	data()[37]	2.934s	passed
jdiv_uniqueNegPos	data()[38]	2.927s	passed
jdiv_uniqueNegNeg	data()[39]	2.933s	passed
irrflConcrete1	data()[3]	3.217s	passed
jdivMultDenom1	data()[40]	2.948s	passed
jdivMultDenom2	data()[41]	2.939s	passed
mod_geZero	data()[42]	2.919s	passed
mod_lessDenom	data()[43]	2.920s	passed
jmod_NumPos	data()[44]	2.912s	passed
jmod_NumNeg	data()[45]	2.927s	passed
jmod_geZero	data()[46]	2.903s	passed
jmodNumZero	data()[47]	2.950s	passed
jmod_pulloutminusNum	data()[48]	2.943s	passed
jmod_pulloutminusDenom	data()[49]	2.907s	passed
irrflConcrete2	data()[4]	3.150s	passed
jmodUnique1	data()[50]	2.954s	passed
jmodUnique2	data()[51]	2.964s	passed
intDivRem	data()[52]	2.899s	passed
jmodjmod	data()[53]	2.933s	passed
jmodDivisible	data()[54]	2.957s	passed
jmodDivisibleRep	data()[55]	2.898s	passed
jdivAddMultDenom	data()[56]	3.033s	passed
jmodAltZero	data()[57]	2.916s	passed
jmodAddMultDenomZero	data()[58]	2.899s	passed
polyDiv_zero	data()[59]	2.901s	passed
cancel_gtPos	data()[5]	3.126s	passed
polyMod_ltdivDenom	data()[60]	2.904s	passed
bsum_empty	data()[61]	2.884s	passed
bsum_induction_upper	data()[62]	2.890s	passed
bsum_induction_lower	data()[63]	2.913s	passed
bsum_num_of_bounds	data()[64]	2.905s	passed
bsum_num_of_bounds2	data()[65]	2.898s	passed
bsum_induction_upper2	data()[66]	2.893s	passed
bsum_induction_upper_concrete	data()[67]	2.893s	passed
bsum_induction_upper_concrete_2	data()[68]	2.903s	passed
bsum_induction_upper2_concrete	data()[69]	2.892s	passed
cancel_gtNeg	data()[6]	3.052s	passed
bsum_induction_lower_concrete	data()[70]	2.899s	passed
bsum_induction_lower2	data()[71]	2.893s	passed
bsum_induction_lower2_concrete	data()[72]	2.895s	passed
bsum_positive	data()[73]	2.966s	passed
bsum_upper_bound	data()[74]	2.962s	passed
bsum_lower_bound	data()[75]	2.930s	passed
bsum_positive_lower_bound_element	data()[76]	2.939s	passed
bsum_sub_same_index	data()[77]	2.927s	passed
bsum_less_same_index	data()[78]	2.953s	passed
bsum_equal_except_one_index	data()[79]	2.925s	passed
moduloIntIsInInt	data()[7]	3.035s	passed
bsum_num_of_is_max	data()[80]	2.920s	passed
bsum_num_of_is_max2	data()[81]	2.916s	passed
bsum_num_of_is_max3	data()[82]	2.915s	passed
bsum_num_of_is_max4	data()[83]	2.922s	passed
bsum_num_of_lt_max	data()[84]	2.911s	passed
bsum_num_of_lt_max2	data()[85]	2.911s	passed
bsum_num_of_lt_max3	data()[86]	2.912s	passed
bsum_num_of_lt_max4	data()[87]	2.905s	passed
bsum_num_of_gt0	data()[88]	2.908s	passed
bsum_num_of_gt0_alt	data()[89]	2.936s	passed
moduloLongIsInLong	data()[8]	2.972s	passed
bsum_add_concrete	data()[90]	2.913s	passed
bprod_all_positive	data()[91]	2.913s	passed
bprod_split	data()[92]	2.903s	passed
powConcrete0	data()[93]	2.900s	passed
powConcrete1	data()[94]	2.911s	passed
powSplitFactor	data()[95]	2.910s	passed
powAdd	data()[96]	2.907s	passed
powMono	data()[97]	2.912s	passed
powMonoConcrete	data()[98]	2.901s	passed
powMonoConcreteRight	data()[99]	2.898s	passed
moduloShortIsInShort	data()[9]	2.964s	passed
Standard output

323        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
342        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.62ms 
535        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548        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)

1504       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1505       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1510       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1511       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2874       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7712       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.18s 
7770       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7799       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.6ns 
7809       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7809       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.2ns 
7814       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10440      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
10443      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11272      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11300      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.76ms 
11314      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11315      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.5ns 
11317      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
13926      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
14732      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
14746      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
14748      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
14748      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133ns 
14749      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17123      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
17123      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
17945      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
17961      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.51ms 
17966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
17966      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.7ns 
17967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20346      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
20346      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21109      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21114      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
21116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21116      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.6ns 
21117      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23414      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
23415      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24240      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.49ms 
24243      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24243      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.6ns 
24244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26508      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
26508      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27292      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
27293      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27293      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111ns 
27294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29536      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
29536      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
30323      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
30327      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.5ns 
30328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
30328      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.7ns 
30330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32564      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
32564      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
33297      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
33299      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 491.3ns 
33301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
33301      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
33302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35531      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
35531      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
36261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
36263      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540.5ns 
36268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
36268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.8ns 
36269      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
38485      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
39215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
39218      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557ns 
39219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
39219      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122ns 
39220      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
41438      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
42186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
42190      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
42194      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
42194      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 550ns 
42195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44429      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
44429      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
45161      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
45234      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.68ms 
45236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
45236      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.4ns 
45237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47451      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
47452      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
48186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
48259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.51ms 
48264      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
48264      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.2ns 
48266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50478      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
50478      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
51203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
51343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 131.12ms 
51347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
51348      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.8ns 
51349      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53559      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
53560      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
54302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
54306      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
54308      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
54308      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.7ns 
54309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56514      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
56515      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
57244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
57247      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
57249      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
57249      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.4ns 
57250      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
59449      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
60172      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
60208      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.53ms 
60210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
60210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.9ns 
60211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62446      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
62446      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
63178      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
63192      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ms 
63196      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
63196      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.5ns 
63197      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65396      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
65396      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
66120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
66133      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
66134      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
66134      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.3ns 
66135      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68324      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
68324      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
69048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
69063      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
69065      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
69065      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
69066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71355      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
71356      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
72078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
72092      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.37ms 
72093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
72094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.8ns 
72094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
74295      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
75018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
75041      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.99ms 
75043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
75043      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118ns 
75044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77238      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
77239      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
77958      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
77960      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
77962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
77962      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
77963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80154      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
80154      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
80879      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
80925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.46ms 
80927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
80927      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
80928      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83128      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
83128      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
83847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
83900      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.04ms 
83903      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
83903      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.7ns 
83904      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86090      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
86090      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
86819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
86862      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.55ms 
86864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
86864      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
86864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89054      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
89055      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
89776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
89783      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
89785      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
89786      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.5ns 
89787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91987      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
91987      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
92713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
92731      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.22ms 
92737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
92737      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.4ns 
92738      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
94928      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
95627      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
95664      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.2ms 
95670      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
95670      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.4ns 
95671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97873      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
97874      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
98570      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
98579      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.52ms 
98581      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
98581      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
98582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
100809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
101505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
101517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ms 
101518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
101518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
101519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
103726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
104425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
104433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
104435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
104435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.1ns 
104436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
106676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
107371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
107375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
107376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
107376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
107377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
109576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
110272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
110282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.83ms 
110283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
110284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
110285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
112506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
113201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
113251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.36ms 
113253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
113253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.7ns 
113254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
115466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
116163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
116179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.97ms 
116181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
116182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.7ns 
116183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
118401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
119098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
119115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.55ms 
119116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
119116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
119117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
121329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
122026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
122043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms 
122044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
122044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
122045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
124263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
124960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
124976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.98ms 
124977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
124977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
124978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
127177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
127883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
127923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.45ms 
127929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
127929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.7ns 
127933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
130157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
130859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
130864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 974.7ns 
130867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
130867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
130869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
133085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
133780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
133784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
133785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
133785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
133786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
135993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
136696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
136704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 
136705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
136705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
136706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
138908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
139609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
139616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.38ms 
139617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
139619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
139620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
141824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
142525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
142543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ms 
142545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
142545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262ns 
142546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
144745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
145439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
145447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.44ms 
145448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
145448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
145448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
147658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
148392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
148396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
148399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
148399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.9ns 
148400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
150620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
151336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
151339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
151340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
151340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
151341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
153531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
154243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
154246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
154247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
154247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.6ns 
154248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
156424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
157138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
157200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.47ms 
157202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
157202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.5ns 
157203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
159380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
160095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
160165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.19ms 
160166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
160166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
160167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
162342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
163061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
163065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
163066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
163066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
163067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
165253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
165967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
165997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.82ms 
165998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
165998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
165999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
168190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
168912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
168954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.84ms 
168955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
168956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
168956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
171135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
171849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
171852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 995ns 
171853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
171853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
171854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
174028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
174740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
174885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 134.73ms 
174888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
174888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.9ns 
174889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
177073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
177792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
177802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.04ms 
177804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
177804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.4ns 
177805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
179981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
180694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
180701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
180702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
180702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
180703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
182870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
183587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
183602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.43ms 
183603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
183603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
183604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
185782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
186494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
186504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
186506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
186506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
186507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
188677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
189386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
189389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
189390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
189391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
189391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
191559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
192275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
192279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
192280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
192280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
192281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
194459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
195172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
195193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.17ms 
195194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
195194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
195195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
197369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
198083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
198098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.05ms 
198099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
198099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
198100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
200269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
200982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
200996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ms 
200997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
200997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
200998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
203173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
203886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
203890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
203891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
203891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
203892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
206065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
206779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
206783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
206785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
206785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.6ns 
206786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
208967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
209682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
209687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
209688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
209688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
209688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
211863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
212577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
212580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
212581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
212581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
212581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
214764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
215476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
215478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 651.2ns 
215479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
215479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
215480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
217655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
218368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
218371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
218372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
218372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
218373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
220550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
221264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
221266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 935.5ns 
221267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
221267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
221268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
223445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
224166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
224232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.15ms 
224234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
224234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.2ns 
224235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
226445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
227162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
227195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.36ms 
227196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
227196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
227197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
229380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
230097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
230125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.66ms 
230127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
230127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
230127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
232309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
233025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
233064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.81ms 
233066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
233066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
233066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
235247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
235963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
235992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.82ms 
235993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
235993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
235994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
238183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
238898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
238946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.54ms 
238947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
238947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
238948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
241126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
241843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
241871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.43ms 
241873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
241873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.9ns 
241874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
244057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
244773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
244791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.77ms 
244792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
244792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
244793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
246967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
247685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
247707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.25ms 
247709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
247709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
247709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
249884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
250603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
250622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.94ms 
250623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
250623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
250624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
252805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
253519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
253545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.35ms 
253546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
253546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
253547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
255719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
256432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
256455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.37ms 
256457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
256457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
256457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
258631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
259343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
259366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.28ms 
259368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
259368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
259369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
261543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
262256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
262279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.28ms 
262280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
262280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
262281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
264454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
265166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
265185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms 
265186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
265186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
265187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
267357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
268069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
268093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.35ms 
268094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
268094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
268095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
270274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
271005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
271029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.31ms 
271031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
271031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.9ns 
271032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
273220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
273935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
273942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.51ms 
273943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
273944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
273944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
276124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
276839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
276856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.79ms 
276857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
276857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
276857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
279038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
279755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
279759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
279760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
279760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
279760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
281941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
282657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
282660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 555.6ns 
282661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
282661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
282661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
284845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
285568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
285570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 706.7ns 
285572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
285572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.5ns 
285573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
287760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
288473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
288480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 
288481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
288481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
288482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
290666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
291382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
291388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ms 
291389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
291389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
291390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
293573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
294289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
294300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.88ms 
294301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
294301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
294302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
296480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
297197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
297201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
297202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
297202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
297203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
299381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
300097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
300099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 481ns 
300100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
300100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
300101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
302279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
302993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
302998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
302999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
302999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
303000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
305180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
305894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
305896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 616.1ns 
305898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
305898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174ns 
305899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
308082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
308796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
308798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 546.7ns 
308799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
308800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
308800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
310979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
311694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
311696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 543.1ns 
311697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
311697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
311698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
313879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
314592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
314595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
314597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
314597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
314597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
316771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
317485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
317493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.41ms 
317494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
317494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
317495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
319675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
320398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
320401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
320402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
320403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
320403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
322583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
323298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
323304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
323305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
323305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
323306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
325481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
326194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
326202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.46ms 
326207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
326207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.3ns 
326208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
328390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
329113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
329128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.86ms 
329130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
329130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.3ns 
329131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
331316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
332037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
332040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
332042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
332042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.3ns 
332043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
334222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
334919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
334922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
334923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
334923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
334923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
337120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
337815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
337819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
337820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
337820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
337821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
340013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
340707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
340723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.69ms 
340724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
340724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
340725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
342925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
343618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
343621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 521.8ns 
343623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
343623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
343624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
345812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
346509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
346545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.39ms 
346547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
346547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
346547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
348742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
349438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
349441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
349443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
349443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
349443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
351643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
352338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
352359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.39ms 
352361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
352361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
352361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
354573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
355267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
355287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.08ms 
355288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
355288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
355289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
357485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
358180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
358203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.26ms 
358204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
358204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
358205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
360400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
361095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
361097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 502.3ns 
361098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
361098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
361099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
363292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
363986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
363991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
363992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
363992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
363993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
366189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
366885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
366888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
366889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
366889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
366889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
369081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
369777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
369780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 802.9ns 
369781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
369781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
369781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
371983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
372683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
372686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 868.29ns 
372687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
372688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.8ns 
372688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
374884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
375581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
375584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
375585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
375585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
375586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
377776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
378473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
378475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
378477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
378477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
378477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
380672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
381371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
381380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.68ms 
381381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
381381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
381382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
383577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
384274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
384285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.19ms 
384286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
384286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
384287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
386458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
387177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
387187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.36ms 
387188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
387189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
387189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
389388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
390092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
390103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.16ms 
390105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
390105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
390105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
392309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
393014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
393019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
393020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
393020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
393020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
395223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
395929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
395935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 
395936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
395936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
395936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
398154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
398860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
398862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 664.6ns 
398863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
398864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
398865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
401067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
401769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
401772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
401773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
401773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
401773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
403968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
404672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
404674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 836.6ns 
404676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
404676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.5ns 
404676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
406909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
407615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
407626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.67ms 
407627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
407627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
407628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
410013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
410716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
410720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
410721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
410721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
410722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
412924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
413650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
413656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
413657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
413657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
413658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
415837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
416559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
416561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.6ns 
416562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
416562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
416563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
418779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
419504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
419506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 641.6ns 
419507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
419507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
419507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
421686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
422409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
422413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
422415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
422415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.9ns 
422416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
424591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
425319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
425322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
425323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
425323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
425324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
427498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
428219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
428223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
428224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
428224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
428224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
430424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
431172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
431174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
431175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
431175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
431176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
433414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
434117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
434122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
434123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
434123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
434123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
436315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
437018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
437020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
437021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
437022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
437022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
439213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
439933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
439943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.16ms 
439944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
439944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
439945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
442123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
442843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
442845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.8ns 
442846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
442846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
442847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
445017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
445739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
445745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
445746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
445746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
445747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
447918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
448641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
448643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 897.4ns 
448644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
448644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
448646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
450815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
451536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
451539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 761.7ns 
451540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
451540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
451540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
453730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
454431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
454437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
454439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
454439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161ns 
454440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
456630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
457354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
457357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
457358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
457358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.5ns 
457359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
459529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
460250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
460253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
460255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
460255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
460255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
462423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
463144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
463147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
463148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
463148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
463149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
465336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
466038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
466043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
466044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
466044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
466044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
468233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
468958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
468972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
468973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
468973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
468974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
471150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
471873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
471888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.82ms 
471889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
471889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
471890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
474057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
474779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
474789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ms 
474790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
474790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
474791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
476982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
477684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
477694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
477696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
477696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
477696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
479882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
480605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
480631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.44ms 
480632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
480632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
480633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
482811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
483535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
483560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.31ms 
483561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
483561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
483561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
485734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
486460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
486483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.59ms 
486484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
486484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
486484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
488679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
489403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
489417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.91ms 
489418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
489418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
489419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
491601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
492329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
492359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.62ms 
492360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
492360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
492361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
494541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
495266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
495312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.04ms 
495314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
495314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.1ns 
495315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
497507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
498234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
498270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.7ms 
498272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
498272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
498272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
500454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
501181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
501221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.37ms 
501223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
501223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
501223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
503418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
504121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
504163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.22ms 
504165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
504165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
504165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
506356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
507080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
507194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.26ms 
507196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
507196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
507196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
509376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
510103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
510113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.88ms 
510115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
510115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
510116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
512313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
513037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
513044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.73ms 
513045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
513045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
513046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
515220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
515945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
515950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
515951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
515951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
515951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
518139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
518843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
518860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.44ms 
518861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
518861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
518862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
521051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
521775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
521785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
521786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
521786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
521787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
523961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
524684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
524687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
524688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
524689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
524689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
526881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
527604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
527621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.14ms 
527622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
527622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
527623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
529797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
530520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
530536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.45ms 
530537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
530537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
530538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
532736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
533461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
533479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.84ms 
533480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
533480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
533481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
535650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
536374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
536376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
536377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
536377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
536378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
538561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
539287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
539291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
539292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
539292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
539293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
541462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
542185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
542191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
542192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
542192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
542192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
544383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
545109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
545115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
545116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
545116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.6ns 
545117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
547284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
548005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
548074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.44ms 
548075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
548075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
548076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
550267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
550993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
551022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.9ms 
551024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
551024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.5ns 
551025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
553202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
553926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
553947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.99ms 
553948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
553948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
553948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
556135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
556859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
556861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 316.7ns 
556862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
556862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
556863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
559038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
559763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
559968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 195.03ms 
559970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
559970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.9ns 
559971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
562168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
562896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
562944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.86ms 
562946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
562946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.9ns 
562947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
565144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
565869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
565871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 287.8ns 
565873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
565873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
565873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
568047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
568772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
568774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 318.3ns 
568775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
568775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
568775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
570962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
571685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
571686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 338.1ns 
571687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
571688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
571688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
573870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
574573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
574575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 450.6ns 
574576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
574576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
574576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
576763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
577487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
577601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.7ms 
577604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
577604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.6ns 
577605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
579846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
580594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
580637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.82ms 
580639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
580639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
580640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
582826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
583558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
583559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
583583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
583613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
583628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
583632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
583636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
583639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
583639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
583641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
583643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
583645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
583647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
583648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
583809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
583810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
583811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
583812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
583813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
583918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
583918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
583919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
583921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
583922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
583923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
584071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
584073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
584074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
584075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
584075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
584076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
584191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
584193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
584194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
584194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
584195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
584196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
584203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
584204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
584205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
584207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
584208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
584209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
584215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
584216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
584217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
584218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
584219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
584219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
584366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
584367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
584396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
584516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
584518     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)'' 
584521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
584523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
584524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
584525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
584526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
584529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
584533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
584535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
584536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
584536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
584537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
584687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
584691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
584693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
584693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
584694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
584695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
584696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
584841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
584845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
584845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
584847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
584847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
584848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
584849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
584851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
584962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
584964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
585069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
585074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
585080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
585081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
585082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
585083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
585086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
585086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
585087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
585089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
585097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
585102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
585203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
585205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
585206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
585208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
585208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
585211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
585211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
585212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
585272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
585277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
585380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
585381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
585383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
585384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
585385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
585386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
585517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
585521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
585524     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)'' 
585525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
585527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
585527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
585528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
585529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
585537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
585543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
585544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
585545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
585643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
585644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
585645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
585646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
585646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
585647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
585751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
585753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
585754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
585755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
585756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
585757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
585757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
585758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
585845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
585846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
585924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
585924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
585925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
585930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
585933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
585938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
586059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
586061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
586061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
586062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
586072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
586153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
589579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
589580     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)'' 
589585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
589586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
589587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
589588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
589588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
589596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
589597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
589598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
589599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
589599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
589689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
589693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
589694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
589695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
589695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
589696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
589697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
589789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
589791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
589791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
589793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
589793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
589794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
589794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
589795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
589870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
589871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
589942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
589946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
589950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
589951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
589952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
589953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
589962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
590040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
590041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
590041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
590042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
590112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
590121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
590122     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)'' 
590123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
590124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
590125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
590125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
590126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
590136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
590137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
590138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
590139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
590139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
590225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
590226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
590227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
590228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
590228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
590316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
590320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
590321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
590322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
590322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
590323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
590323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
590419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
590420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
590421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
590422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
590422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
590423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
590423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
590424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
590424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
590425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
590426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
590426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
590427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
590427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
590428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
590513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
590514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
590520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
590596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
590675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
590677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
590677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
590678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
590679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
590679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
590679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
590680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
590681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
590765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
590771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
590859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
590860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
590860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
590861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
590862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
590862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
590863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
590863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
590868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
590869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
590947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
590953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
590958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
591057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
591058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
591059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
591060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
591060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
591061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
591061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
591062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
591116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
591117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
591118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
591118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
591119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
591125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
591130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
591243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
591386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
591388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
591388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
591389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
591551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
591637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
591638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
594603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
594608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
594609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
594610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
594610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
594720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
594721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
594722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
594723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
594724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
594826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
597794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
600903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
600907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
600908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
600908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
600909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
601018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
601020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
601021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
601021     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)' ...' 
601023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
602158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
602158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.4ns 
602158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
604414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
605161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
605162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ns 
605163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
605183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
605199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
605201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
605203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
605203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
605207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
605208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
605211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
605213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
605214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
605221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
605223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
605223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
605267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
605268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
605268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
605269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
605269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
605332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
605332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
605334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
605335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
605335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
605338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
605339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
605339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
605340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
605341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
605342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
605419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
605420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
605421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
605422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
605423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
605423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
605504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
605505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
605506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
605506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
605507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
605508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
605508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
605509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
605509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
605510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
605510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
605511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
605511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
605512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
605512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
605512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
605513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
605514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
605515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
605517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
605551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
605553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
605607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
605609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
605610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
605611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
605612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
605613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
605656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
605658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
605659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
605661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
605662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
605663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
605663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
605707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
605710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
605713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
605764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
605816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
605816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.2ns 
605817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
608018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
608760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
608790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.96ms