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

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
198
tests
failures
ignored
13m5.47s
duration
100%
successful
Tests
Standard output
Tests

Test	Method name	Duration	Result
powPositive	data()[100]	3.827s	passed
powPositiveConcrete	data()[101]	3.804s	passed
powGeq1Concrete	data()[102]	3.793s	passed
pow2InIntLower	data()[103]	3.784s	passed
pow2InIntUpper	data()[104]	3.796s	passed
logSelfConcrete	data()[105]	3.798s	passed
log1Concrete	data()[106]	3.776s	passed
logProduct	data()[107]	3.750s	passed
logTimesBaseConcrete	data()[108]	3.772s	passed
logProdIdentity	data()[109]	3.821s	passed
moduloByteIsInByte	data()[10]	3.910s	passed
logProdIdentityConcrete	data()[110]	3.838s	passed
logPowIdentity	data()[111]	3.804s	passed
logPowIdentityConcrete	data()[112]	3.808s	passed
logPositive	data()[113]	3.884s	passed
logPositiveConcrete	data()[114]	3.784s	passed
logMono	data()[115]	3.831s	passed
logMonoConcrete	data()[116]	3.781s	passed
powLogLess	data()[117]	3.818s	passed
powLogMore2	data()[118]	3.808s	passed
logLessThanPow	data()[119]	3.864s	passed
moduloCharIsInChar	data()[11]	3.858s	passed
logLessThanPowConcrete	data()[120]	3.850s	passed
logSqueeze	data()[121]	3.817s	passed
ifthenelse_equals	data()[122]	3.828s	passed
ifthenelse_equals_1	data()[123]	3.806s	passed
ifthenelse_equals_2	data()[124]	3.786s	passed
disjointWithSingleton1	data()[125]	3.876s	passed
disjointWithSingleton2	data()[126]	3.820s	passed
disjointArrayRanges	data()[127]	3.799s	passed
disjointArrayRangeAllFields1	data()[128]	3.827s	passed
disjointArrayRangeAllFields2	data()[129]	3.786s	passed
div_unique1	data()[12]	3.942s	passed
seqSelfDefinition	data()[130]	3.811s	passed
seqOutsideValue	data()[131]	3.803s	passed
castedGetAny	data()[132]	3.799s	passed
seqGetAlphaCast	data()[133]	3.809s	passed
getOfSeqSingleton	data()[134]	3.764s	passed
getOfSeqSingletonConcrete	data()[135]	3.829s	passed
getOfSeqConcat	data()[136]	3.827s	passed
getOfSeqSub	data()[137]	3.855s	passed
getOfSeqReverse	data()[138]	3.797s	passed
lenOfSeqEmpty	data()[139]	3.846s	passed
div_unique2	data()[13]	3.869s	passed
lenOfSeqSingleton	data()[140]	3.908s	passed
lenOfSeqConcat	data()[141]	3.909s	passed
lenOfSeqSub	data()[142]	3.951s	passed
lenOfSeqReverse	data()[143]	3.874s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.849s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.862s	passed
getOfSeqSingletonEQ	data()[146]	3.831s	passed
getOfSeqConcatEQ	data()[147]	3.872s	passed
getOfSeqSubEQ	data()[148]	3.874s	passed
getOfSeqReverseEQ	data()[149]	3.848s	passed
div_exists	data()[14]	3.987s	passed
lenOfSeqEmptyEQ	data()[150]	3.832s	passed
lenOfSeqSingletonEQ	data()[151]	3.875s	passed
lenOfSeqConcatEQ	data()[152]	3.806s	passed
lenOfSeqSubEQ	data()[153]	3.779s	passed
lenOfSeqReverseEQ	data()[154]	3.793s	passed
getOfSeqDefEQ	data()[155]	3.815s	passed
lenOfSeqDefEQ	data()[156]	3.814s	passed
seqConcatWithSeqEmpty1	data()[157]	3.783s	passed
seqConcatWithSeqEmpty2	data()[158]	3.827s	passed
seqReverseOfSeqEmpty	data()[159]	3.809s	passed
div_one	data()[15]	3.899s	passed
subSeqComplete	data()[160]	3.806s	passed
subSeqTailR	data()[161]	3.802s	passed
subSeqTailL	data()[162]	3.877s	passed
subSeqTailEQR	data()[163]	3.857s	passed
subSeqTailEQL	data()[164]	3.849s	passed
seqDef_split	data()[165]	3.837s	passed
seqDef_induction_upper	data()[166]	3.845s	passed
seqDef_induction_upper_concrete	data()[167]	3.847s	passed
seqDef_induction_lower	data()[168]	3.888s	passed
seqDef_induction_lower_concrete	data()[169]	3.833s	passed
jdiv_one	data()[16]	3.853s	passed
seqDef_split_in_three	data()[170]	3.896s	passed
seqDef_empty	data()[171]	3.815s	passed
seqDef_one_summand	data()[172]	3.819s	passed
seqDef_lower_equals_upper	data()[173]	3.807s	passed
seqDefOfSeq	data()[174]	3.902s	passed
seqSelfDefinitionEQ2	data()[175]	3.817s	passed
indexOfSeqSingleton	data()[176]	3.849s	passed
indexOfSeqConcatFirst	data()[177]	3.827s	passed
indexOfSeqConcatSecond	data()[178]	3.824s	passed
indexOfSeqSub	data()[179]	3.812s	passed
div_zero	data()[17]	3.885s	passed
lenOfArray2seq	data()[180]	3.788s	passed
getAnyOfArray2seq	data()[181]	3.788s	passed
getOfArray2seq	data()[182]	3.804s	passed
getAnyOfNPermInv	data()[183]	3.802s	passed
seqNPermRange	data()[184]	3.843s	passed
seqPermTrans	data()[185]	3.825s	passed
seqPermRefl	data()[186]	3.832s	passed
seqPermSplit	data()[187]	3.829s	passed
seqNPermRight	data()[188]	3.956s	passed
seqPermFromSwap	data()[189]	3.924s	passed
divResZero1	data()[18]	3.884s	passed
seqPermTransAlt0	data()[190]	3.816s	passed
seqPermTransAlt1	data()[191]	3.810s	passed
seqPermTransAlt2	data()[192]	3.864s	passed
seqPermTransAlt3	data()[193]	3.819s	passed
seqPermForall	data()[194]	4.016s	passed
seqPermExists	data()[195]	3.920s	passed
schiffl_lemma_2	data()[196]	25.661s	passed
schiffl_thm_1	data()[197]	4.783s	passed
eqSameSeq	data()[198]	4.042s	passed
divResZero2	data()[19]	3.901s	passed
eqTermCut	data()[1]	4.677s	passed
divResOne1	data()[20]	3.877s	passed
divResOne2	data()[21]	3.939s	passed
div_cancel1	data()[22]	3.865s	passed
div_cancel2	data()[23]	3.834s	passed
divAddMultDenom	data()[24]	3.891s	passed
divMinus	data()[25]	3.864s	passed
divMinusDenom	data()[26]	3.871s	passed
divLeastDPos	data()[27]	3.947s	passed
divLeastDNeg	data()[28]	3.885s	passed
divGreatestDPos	data()[29]	3.867s	passed
equivAllRight	data()[2]	4.389s	passed
divGreatestDNeg	data()[30]	3.876s	passed
divIncreasingPos	data()[31]	3.874s	passed
divIncreasingNeg	data()[32]	3.853s	passed
jdiv_zero	data()[33]	3.865s	passed
jdivPulloutMinusNum	data()[34]	3.866s	passed
jdivPulloutMinusDenom	data()[35]	3.928s	passed
jdiv_uniquePosPos	data()[36]	3.919s	passed
jdiv_uniquePosNeg	data()[37]	3.846s	passed
jdiv_uniqueNegPos	data()[38]	3.827s	passed
jdiv_uniqueNegNeg	data()[39]	3.856s	passed
irrflConcrete1	data()[3]	4.232s	passed
jdivMultDenom1	data()[40]	3.830s	passed
jdivMultDenom2	data()[41]	3.818s	passed
mod_geZero	data()[42]	3.891s	passed
mod_lessDenom	data()[43]	3.785s	passed
jmod_NumPos	data()[44]	3.812s	passed
jmod_NumNeg	data()[45]	3.814s	passed
jmod_geZero	data()[46]	3.810s	passed
jmodNumZero	data()[47]	3.860s	passed
jmod_pulloutminusNum	data()[48]	3.860s	passed
jmod_pulloutminusDenom	data()[49]	3.830s	passed
irrflConcrete2	data()[4]	4.018s	passed
jmodUnique1	data()[50]	3.853s	passed
jmodUnique2	data()[51]	3.853s	passed
intDivRem	data()[52]	3.783s	passed
jmodjmod	data()[53]	3.815s	passed
jmodDivisible	data()[54]	3.788s	passed
jmodDivisibleRep	data()[55]	3.911s	passed
jdivAddMultDenom	data()[56]	3.960s	passed
jmodAltZero	data()[57]	3.872s	passed
jmodAddMultDenomZero	data()[58]	3.785s	passed
polyDiv_zero	data()[59]	3.787s	passed
cancel_gtPos	data()[5]	3.957s	passed
polyMod_ltdivDenom	data()[60]	3.809s	passed
bsum_empty	data()[61]	3.804s	passed
bsum_induction_upper	data()[62]	3.835s	passed
bsum_induction_lower	data()[63]	3.871s	passed
bsum_num_of_bounds	data()[64]	3.875s	passed
bsum_num_of_bounds2	data()[65]	3.800s	passed
bsum_induction_upper2	data()[66]	3.818s	passed
bsum_induction_upper_concrete	data()[67]	3.774s	passed
bsum_induction_upper_concrete_2	data()[68]	3.810s	passed
bsum_induction_upper2_concrete	data()[69]	3.770s	passed
cancel_gtNeg	data()[6]	3.947s	passed
bsum_induction_lower_concrete	data()[70]	3.798s	passed
bsum_induction_lower2	data()[71]	3.789s	passed
bsum_induction_lower2_concrete	data()[72]	3.819s	passed
bsum_positive	data()[73]	3.834s	passed
bsum_upper_bound	data()[74]	3.829s	passed
bsum_lower_bound	data()[75]	3.814s	passed
bsum_positive_lower_bound_element	data()[76]	3.919s	passed
bsum_sub_same_index	data()[77]	3.835s	passed
bsum_less_same_index	data()[78]	3.842s	passed
bsum_equal_except_one_index	data()[79]	3.814s	passed
moduloIntIsInInt	data()[7]	3.907s	passed
bsum_num_of_is_max	data()[80]	3.833s	passed
bsum_num_of_is_max2	data()[81]	3.825s	passed
bsum_num_of_is_max3	data()[82]	3.869s	passed
bsum_num_of_is_max4	data()[83]	3.815s	passed
bsum_num_of_lt_max	data()[84]	3.879s	passed
bsum_num_of_lt_max2	data()[85]	3.855s	passed
bsum_num_of_lt_max3	data()[86]	3.835s	passed
bsum_num_of_lt_max4	data()[87]	3.832s	passed
bsum_num_of_gt0	data()[88]	3.837s	passed
bsum_num_of_gt0_alt	data()[89]	3.790s	passed
moduloLongIsInLong	data()[8]	3.932s	passed
bsum_add_concrete	data()[90]	3.826s	passed
bprod_all_positive	data()[91]	3.785s	passed
bprod_split	data()[92]	3.845s	passed
powConcrete0	data()[93]	3.805s	passed
powConcrete1	data()[94]	3.799s	passed
powSplitFactor	data()[95]	3.862s	passed
powAdd	data()[96]	3.814s	passed
powMono	data()[97]	3.828s	passed
powMonoConcrete	data()[98]	3.811s	passed
powMonoConcreteRight	data()[99]	3.788s	passed
moduloShortIsInShort	data()[9]	3.845s	passed
Standard output

592        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
618        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.28ms 
857        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
875        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)

1898       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1903       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1907       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1907       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3582       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10105      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.25s 
10175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10213      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.6ns 
10227      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10227      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.31ns 
10232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13667      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
13670      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14857      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14892      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.21ms 
14910      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14911      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 606.51ns 
14913      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18204      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
18206      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
19282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19296      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
19298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19298      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.01ns 
19300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
22485      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
23520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
23527      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
23531      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23531      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.01ns 
23533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26535      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
26535      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
27540      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
27546      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
27551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
27551      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 566.72ns 
27553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30495      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
30495      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
31463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
31506      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.56ms 
31508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
31508      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.91ns 
31509      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
34485      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
35433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
35452      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms 
35456      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
35457      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420.82ns 
35458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38389      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
38390      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
39356      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
39361      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.32ns 
39364      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
39364      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.01ns 
39365      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
42310      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
43290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
43293      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 716.73ns 
43295      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
43295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.11ns 
43296      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46178      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
46179      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
47135      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
47138      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.12ns 
47140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
47140      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.71ns 
47141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50085      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
50085      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
51044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
51047      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 664.03ns 
51050      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
51050      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.31ns 
51051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53940      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
53940      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
54903      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
54906      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 704.42ns 
54908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
54909      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.11ns 
54910      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57800      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
57800      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
58772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
58842      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.73ms 
58854      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
58856      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.12ms 
58858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61728      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
61728      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
62686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
62719      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.51ms 
62722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
62722      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.6ns 
62724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65626      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
65627      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
66558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
66702      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 134.19ms 
66709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
66709      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.81ns 
66710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
69620      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
70600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
70606      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
70609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
70609      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.71ns 
70611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73497      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
73498      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
74456      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
74459      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
74461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
74461      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.61ns 
74462      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77348      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
77348      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
78303      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
78344      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.36ms 
78347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
78347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.21ns 
78348      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81285      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
81285      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
82214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
82228      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.29ms 
82230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
82230      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131ns 
82231      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85140      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
85140      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
86112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
86128      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.74ms 
86131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
86132      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 929.53ns 
86138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89040      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
89041      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
89993      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
90007      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.88ms 
90008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
90009      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.5ns 
90010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92968      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
92968      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
93933      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
93946      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.65ms 
93948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
93948      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.31ns 
93949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96864      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
96864      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
97790      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
97811      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.42ms 
97813      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
97813      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.6ns 
97814      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
100692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
101642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
101645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
101647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
101647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.41ns 
101648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
104535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
105497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
105536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.34ms 
105539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
105539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.21ns 
105541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
108387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
109347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
109400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.34ms 
109403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
109404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.82ns 
109405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
112316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
113237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
113273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.75ms 
113275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
113275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.91ns 
113276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
116164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
117201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
117219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.11ms 
117225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
117225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 459.92ns 
117227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
120135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
121089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
121107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.68ms 
121110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
121110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.72ns 
121111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
124004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
124959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
124975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.99ms 
124982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
124983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 677.53ns 
124984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
127922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
128847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
128856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
128858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
128858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.1ns 
128863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
131764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
132721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
132730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.57ms 
132733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
132733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.22ns 
132734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
135619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
136576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
136584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
136585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
136585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.6ns 
136586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
139454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
140444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
140448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
140450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
140450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.6ns 
140451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
143375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
144302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
144314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.08ms 
144317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
144317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.01ns 
144318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
147242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
148203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
148241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.35ms 
148244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
148245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.81ns 
148246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
151143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
152145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
152163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.47ms 
152164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
152164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.6ns 
152165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
155039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
155991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
156008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ms 
156010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
156010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.61ns 
156011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
158882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
159818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
159835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 
159837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
159837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.3ns 
159838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
162719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
163669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
163691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.07ms 
163693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
163693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.7ns 
163694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
166541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
167484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
167521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.59ms 
167522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
167523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
167523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
170368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
171333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
171339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
171342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
171342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.01ns 
171343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
174235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
175226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
175230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
175232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
175232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
175233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
178092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
179008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
179015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
179017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
179017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
179018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
181867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
182811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
182826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms 
182829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
182829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.21ns 
182831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
185679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
186623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
186641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.92ms 
186643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
186643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.2ns 
186644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
189507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
190442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
190451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.48ms 
190453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
190453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.6ns 
190454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
193381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
194306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
194311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
194319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
194319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.71ns 
194322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
197229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
198173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
198176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
198178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
198178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
198179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
201015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
202003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
202007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
202009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
202009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.5ns 
202010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
204852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
205794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
205859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.94ms 
205861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
205861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.61ns 
205863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
208726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
209636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
209712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.92ms 
209714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
209714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.81ns 
209715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
212558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
213492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
213495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
213496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
213496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
213497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
216317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
217252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
217308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.92ms 
217313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
217318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.71ms 
217320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
220131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
221074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
221098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.59ms 
221100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
221100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.1ns 
221101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
224033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
225005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
225009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
225011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
225012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.21ns 
225013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
227870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
228820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
228969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 135.95ms 
228972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
228972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.71ns 
228973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
231891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
232832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
232841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.41ms 
232843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
232843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
232844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
235679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
236620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
236626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
236628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
236628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
236629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
239484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
240397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
240413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.69ms 
240414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
240414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
240415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
243267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
244207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
244219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
244225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
244225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.31ns 
244226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
247090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
248024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
248028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
248029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
248029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
248030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
250855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
251858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
251863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
251864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
251864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
251865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
254795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
255717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
255734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ms 
255735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
255735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
255736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
258646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
259594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
259608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.39ms 
259610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
259610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
259611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
262450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
263395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
263408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.34ms 
263409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
263410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
263410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
266248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
267223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
267226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
267228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
267229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.21ns 
267230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
270085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
270997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
271001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
271002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
271002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
271003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
273865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
274805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
274810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
274811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
274811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
274812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
277639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
278578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
278580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
278582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
278582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
278583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
281425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
282376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
282379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 657.42ns 
282380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
282380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
282381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
285248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
286164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
286168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
286169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
286169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
286170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
289044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
289983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
289986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 803.82ns 
289987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
289987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
289988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
292840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
293783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
293820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.77ms 
293821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
293822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.9ns 
293823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
296672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
297614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
297649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.96ms 
297651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
297651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
297652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
300522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
301436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
301463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.16ms 
301467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
301467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.51ns 
301468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
304396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
305343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
305382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.37ms 
305384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
305384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
305385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
308248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
309196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
309217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.92ms 
309218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
309219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
309220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
312077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
313020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
313059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.13ms 
313061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
313062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.61ns 
313063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
315940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
316853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
316873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.46ms 
316875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
316875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
316876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
319736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
320691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
320707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.41ms 
320708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
320708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
320709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
323570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
324514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
324532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.05ms 
324533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
324533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
324534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
327423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
328385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
328400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.09ms 
328402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
328402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
328403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
331273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
332194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
332215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.75ms 
332216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
332216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
332217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
335109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
336075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
336094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.19ms 
336096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
336096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
336097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
338981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
339930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
339949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.59ms 
339951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
339951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
339952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
342814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
343766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
343784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.38ms 
343785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
343785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
343786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
346645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
347600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
347616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.9ms 
347618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
347618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
347619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
350461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
351435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
351453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.22ms 
351456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
351456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.71ns 
351457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
354277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
355226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
355244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.46ms 
355245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
355245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
355246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
358078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
359063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
359069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
359070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
359071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
359071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
361923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
362841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
362854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.23ms 
362856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
362856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
362856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
365742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
366696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
366700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
366701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
366701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
366702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
369544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
370497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
370504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.42ns 
370506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
370506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
370507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
373354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
374301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
374304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 783.37ns 
374305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
374305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.61ns 
374306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
377177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
378158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
378166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
378167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
378167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
378168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
381051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
381973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
381979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.55ms 
381980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
381980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
381981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
384850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
385796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
385807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.66ms 
385808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
385808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
385809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
388649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
389614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
389618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
389619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
389619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
389620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
392462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
393403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
393406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 562.72ns 
393408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
393408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.5ns 
393409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
396310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
397228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
397233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
397235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
397235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
397235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
400093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
401035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
401037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.82ns 
401042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
401042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
401043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
403881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
404831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
404833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570.62ns 
404835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
404835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
404836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
407669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
408615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
408617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.02ns 
408618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
408618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
408619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
411498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
412409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
412413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
412414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
412414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
412415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
415263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
416204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
416212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
416213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
416213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
416214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
419037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
419984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
419987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
419989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
419989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
419989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
422792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
423731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
423737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.93ms 
423738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
423738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
423739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
426590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
427505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
427509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
427511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
427511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
427512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
430366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
431316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
431330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.06ms 
431331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
431331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
431332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
434199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
435165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
435168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
435170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
435170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
435171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
438019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
438969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
438972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
438973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
438974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
438974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
441851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
442777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
442781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
442782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
442782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
442783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
445698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
446650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
446664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
446666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
446666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
446667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
449500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
450443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
450448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 379.81ns 
450450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
450450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
450451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
453310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
454249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
454280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.69ms 
454281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
454281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
454282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
457139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
458057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
458060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
458062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
458062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
458063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
460916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
461860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
461878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.77ms 
461879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
461879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
461880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
464721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
465669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
465686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.46ms 
465687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
465687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
465688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
468588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
469529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
469550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.96ms 
469552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
469552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
469553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
472450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
473398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
473401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 528.61ns 
473402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
473402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
473403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
476265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
477210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
477216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
477219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
477219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
477220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
480122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
481042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
481045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
481047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
481047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
481047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
483895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
484847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
484852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 910.12ns 
484854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
484854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
484855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
487687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
488635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
488638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 801.92ns 
488641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
488641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.41ns 
488642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
491552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
492512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
492515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
492517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
492517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
492518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
495371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
496333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
496336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
496337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
496337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
496338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
499196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
500125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
500134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.39ms 
500135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
500135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
500137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
502998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
503954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
503962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
503963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
503963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
503964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
506785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
507739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
507746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
507749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
507750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.04ms 
507751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
510596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
511550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
511558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.78ms 
511560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
511560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
511561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
514385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
515356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
515361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
515362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
515363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
515363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
518229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
519156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
519161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.66ms 
519162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
519162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
519163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
522011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
522966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
522969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 855.22ns 
522970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
522970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
522971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
525803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
526731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
526734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
526735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
526735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
526736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
529601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
530560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
530563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
530564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
530564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
530565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
533433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
534369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
534386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.64ms 
534391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
534391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
534392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
537271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
538239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
538244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
538245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
538245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
538246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
541103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
542034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
542041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
542043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
542043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
542044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
544918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
545884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
545887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 799.42ns 
545889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
545889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 501.31ns 
545890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
548816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
549793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
549796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 656.01ns 
549797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
549797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
549798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
552742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
553701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
553705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
553706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
553706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
553707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
556677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
557651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
557655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 860.32ns 
557656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
557656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
557657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
560564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
561526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
561529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
561530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
561531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
561531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
564389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
565375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
565378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
565379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
565379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
565380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
568233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
569236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
569241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
569242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
569242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
569243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
572111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
573068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
573071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 994.82ns 
573073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
573073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
573073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
575939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
576931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
576944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.35ms 
576945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
576945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
576946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
579834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
580815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
580818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 535.41ns 
580819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
580819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
580820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
583695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
584659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
584665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
584667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
584667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
584668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
587560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
588495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
588497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 871.72ns 
588499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
588499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
588500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
591380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
592370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
592373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 708.41ns 
592374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
592374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
592375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
595225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
596174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
596178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
596180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
596180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
596181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
599027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
599955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
599958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
599959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
599959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
599960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
602794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
603748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
603751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
603752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
603752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
603753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
606609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
607563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
607566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
607567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
607567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
607568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
610421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
611375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
611379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
611381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
611381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
611381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
614200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
615154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
615163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
615164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
615164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
615165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
618026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
618981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
618990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.14ms 
618991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
618991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
618992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
621830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
622792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
622798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
622800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
622800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
622801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
625642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
626598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
626605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
626606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
626606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
626607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
629460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
630395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
630406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.93ms 
630408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
630408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
630409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
633311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
634271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
634283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.09ms 
634284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
634284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
634285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
637170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
638129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
638140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.54ms 
638141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
638141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
638142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
641017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
641981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
641989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.62ms 
641991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
641991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
641991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
644842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
645803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
645826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.45ms 
645828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
645828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
645829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
648685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
649645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
649671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.99ms 
649673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
649673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
649674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
652561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
653495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
653518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.25ms 
653519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
653519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
653520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
656392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
657384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
657406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.58ms 
657407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
657408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
657408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
660260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
661217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
661239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.82ms 
661241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
661241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
661242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
664123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
665079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
665134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.95ms 
665136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
665136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
665137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
667987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
668945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
668950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
668952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
668952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
668952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
671802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
672763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
672769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
672770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
672770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
672771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
675610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
676572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
676576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
676577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
676577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
676578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
679505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
680463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
680478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.54ms 
680480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
680480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
680481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
683329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
684288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
684295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
684296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
684297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
684297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
687161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
688141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
688145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
688146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
688146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
688147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
691000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
691960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
691972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
691973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
691973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
691974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
694821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
695783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
695795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
695797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
695797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
695798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
698634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
699592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
699607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.41ms 
699609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
699609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
699609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
702434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
703392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
703395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 916.51ns 
703396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
703397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
703397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
706224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
707180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
707183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
707185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
707185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
707186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
710028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
710982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
710988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms 
710989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
710989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
710990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
713827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
714784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
714789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
714791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
714791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
714792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
717629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
718585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
718632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.13ms 
718634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
718634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
718635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
721479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
722436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
722457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.88ms 
722458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
722458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
722459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
725318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
726276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
726289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
726290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
726290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
726291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
729158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
730117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
730119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 189.2ns 
730120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
730120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
730121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
732976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
733971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
734074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.81ms 
734075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
734076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
734077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
736997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
737959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
737999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.54ms 
738000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
738000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
738001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
740850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
741812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
741814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 311.2ns 
741815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
741815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
741816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
744686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
745622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
745624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 263.7ns 
745626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
745626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
745626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
748523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
749486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
749488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 248.5ns 
749490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
749490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
749491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
752348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
753306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
753308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 428.91ns 
753309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
753309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
753310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
756247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
757214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
757312     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
757323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.9ms 
757325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
757326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.3ns 
757327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
760216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
761189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
761243     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
761244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.04ms 
761245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
761245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
761246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
764168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
765132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
765134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
765164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
765224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
765249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
765256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
765276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
765278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
765281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
765282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
765290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
765291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
765297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
765300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
765501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
765502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
765504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
765504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
765506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
765618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
765620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
765621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
765622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
765623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
765625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
765802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
765803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
765805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
765806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
765807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
765808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
765946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
765947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
765949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
765950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
765950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
765952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
765960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
765960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
765961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
765963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
765964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
765966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
765973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
765974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
765975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
765976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
765977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
765978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
766120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
766121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
766122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
766260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
766261     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)'' 
766263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
766265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
766267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
766268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
766269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
766270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
766274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
766275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
766276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
766277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
766279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
766399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
766403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
766404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
766405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
766406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
766407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
766409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
766544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
766545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
766546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
766548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
766549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
766549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
766550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
766551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
766664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
766665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
766770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
766775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
766781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
766782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
766785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
766786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
766787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
766787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
766788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
766789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
766798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
766805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
766921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
766922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
766924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
766925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
766926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
766926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
766927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
766928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
766992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
766998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
767115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
767116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
767117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
767118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
767119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
767121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
767280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
767284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
767286     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)'' 
767288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
767291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
767292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
767293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
767293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
767304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
767310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
767311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
767312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
767433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
767434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
767435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
767437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
767437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
767439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
767570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
767572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
767573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
767574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
767575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
767575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
767576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
767577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
767753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
767755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
767861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
767861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
767862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
767868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
767873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
767880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
768051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
768052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
768052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
768053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
768066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
768172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
772249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
772250     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)'' 
772255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
772256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
772257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
772258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
772259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
772322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
772323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
772324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
772325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
772326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
772433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
772437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
772438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
772440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
772440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
772441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
772442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
772551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
772552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
772553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
772554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
772555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
772556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
772557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
772558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
772645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
772646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
772729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
772734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
772739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
772740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
772741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
772742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
772754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
772846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
772848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
772849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
772850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
772932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
772943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
772944     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)'' 
772945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
772946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
772947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
772948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
772948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
772961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
772962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
772963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
772964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
772965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
773065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
773066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
773068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
773069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
773070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
773174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
773180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
773181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
773182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
773183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
773183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
773184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
773298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
773299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
773300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
773301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
773302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
773303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
773304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
773304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
773305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
773306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
773307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
773308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
773309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
773309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
773310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
773412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
773414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
773421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
773510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
773601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
773603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
773604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
773605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
773606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
773607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
773607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
773608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
773609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
773713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
773722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
773825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
773826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
773827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
773828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
773829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
773829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
773829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
773830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
773836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
773837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
773929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
773935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
773941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
774056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
774057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
774058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
774059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
774059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
774060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
774060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
774061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
774124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
774125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
774126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
774126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
774127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
774134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
774140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
774329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
774431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
774431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
774432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
774433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
774629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
774731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
774732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
778237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
778242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
778243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
778244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
778245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
778376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
778376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
778377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
778378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
778379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
778500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
781881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
785468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
785472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
785473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
785474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
785475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
785661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
785661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
785662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
785663     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)' ...' 
785664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
786906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
786906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
786907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
789880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
790864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
790865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
790866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
790877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
790890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
790893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
790896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
790898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
790904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
790905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
790910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
790910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
790913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
790925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
790927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
790929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
790984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
790985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
790986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
790987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
790987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
791067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
791068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
791069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
791071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
791072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
791077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
791078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
791079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
791079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
791080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
791081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
791179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
791180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
791181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
791182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
791183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
791184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
791285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
791286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
791286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
791287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
791288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
791289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
791289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
791290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
791291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
791291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
791292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
791292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
791293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
791294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
791294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
791295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
791295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
791296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
791297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
791300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
791346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
791347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
791410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
791411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
791412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
791415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
791416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
791417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
791478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
791482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
791483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
791484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
791485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
791487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
791488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
791548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
791551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
791555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
791627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
791690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
791691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.11ms 
791692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
794688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
794688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
795711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
795729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.83ms