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

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

Test	Method name	Duration	Result
powPositive	data()[100]	3.106s	passed
powPositiveConcrete	data()[101]	3.118s	passed
powGeq1Concrete	data()[102]	3.061s	passed
pow2InIntLower	data()[103]	3.018s	passed
pow2InIntUpper	data()[104]	3.045s	passed
logSelfConcrete	data()[105]	3.116s	passed
log1Concrete	data()[106]	3.176s	passed
logProduct	data()[107]	3.055s	passed
logTimesBaseConcrete	data()[108]	3.128s	passed
logProdIdentity	data()[109]	3.071s	passed
moduloByteIsInByte	data()[10]	3.215s	passed
logProdIdentityConcrete	data()[110]	3.080s	passed
logPowIdentity	data()[111]	3.151s	passed
logPowIdentityConcrete	data()[112]	3.336s	passed
logPositive	data()[113]	3.095s	passed
logPositiveConcrete	data()[114]	3.081s	passed
logMono	data()[115]	3.162s	passed
logMonoConcrete	data()[116]	3.021s	passed
powLogLess	data()[117]	3.115s	passed
powLogMore2	data()[118]	3.205s	passed
logLessThanPow	data()[119]	3.282s	passed
moduloCharIsInChar	data()[11]	3.241s	passed
logLessThanPowConcrete	data()[120]	3.204s	passed
logSqueeze	data()[121]	3.324s	passed
ifthenelse_equals	data()[122]	3.058s	passed
ifthenelse_equals_1	data()[123]	3.140s	passed
ifthenelse_equals_2	data()[124]	3.027s	passed
disjointWithSingleton1	data()[125]	3.088s	passed
disjointWithSingleton2	data()[126]	3.117s	passed
disjointArrayRanges	data()[127]	3.129s	passed
disjointArrayRangeAllFields1	data()[128]	3.097s	passed
disjointArrayRangeAllFields2	data()[129]	3.091s	passed
div_unique1	data()[12]	3.231s	passed
seqSelfDefinition	data()[130]	3.140s	passed
seqOutsideValue	data()[131]	3.034s	passed
castedGetAny	data()[132]	3.139s	passed
seqGetAlphaCast	data()[133]	3.167s	passed
getOfSeqSingleton	data()[134]	3.353s	passed
getOfSeqSingletonConcrete	data()[135]	3.101s	passed
getOfSeqConcat	data()[136]	3.100s	passed
getOfSeqSub	data()[137]	3.153s	passed
getOfSeqReverse	data()[138]	3.078s	passed
lenOfSeqEmpty	data()[139]	3.223s	passed
div_unique2	data()[13]	3.312s	passed
lenOfSeqSingleton	data()[140]	3.209s	passed
lenOfSeqConcat	data()[141]	3.489s	passed
lenOfSeqSub	data()[142]	3.385s	passed
lenOfSeqReverse	data()[143]	3.155s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.208s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.075s	passed
getOfSeqSingletonEQ	data()[146]	3.061s	passed
getOfSeqConcatEQ	data()[147]	3.094s	passed
getOfSeqSubEQ	data()[148]	3.079s	passed
getOfSeqReverseEQ	data()[149]	3.226s	passed
div_exists	data()[14]	3.316s	passed
lenOfSeqEmptyEQ	data()[150]	3.204s	passed
lenOfSeqSingletonEQ	data()[151]	3.242s	passed
lenOfSeqConcatEQ	data()[152]	3.153s	passed
lenOfSeqSubEQ	data()[153]	3.129s	passed
lenOfSeqReverseEQ	data()[154]	3.179s	passed
getOfSeqDefEQ	data()[155]	3.082s	passed
lenOfSeqDefEQ	data()[156]	3.169s	passed
seqConcatWithSeqEmpty1	data()[157]	3.051s	passed
seqConcatWithSeqEmpty2	data()[158]	3.183s	passed
seqReverseOfSeqEmpty	data()[159]	3.101s	passed
div_one	data()[15]	3.249s	passed
subSeqComplete	data()[160]	3.045s	passed
subSeqTailR	data()[161]	3.169s	passed
subSeqTailL	data()[162]	3.085s	passed
subSeqTailEQR	data()[163]	3.156s	passed
subSeqTailEQL	data()[164]	3.068s	passed
seqDef_split	data()[165]	3.260s	passed
seqDef_induction_upper	data()[166]	3.096s	passed
seqDef_induction_upper_concrete	data()[167]	3.057s	passed
seqDef_induction_lower	data()[168]	3.132s	passed
seqDef_induction_lower_concrete	data()[169]	3.053s	passed
jdiv_one	data()[16]	3.260s	passed
seqDef_split_in_three	data()[170]	3.063s	passed
seqDef_empty	data()[171]	3.151s	passed
seqDef_one_summand	data()[172]	3.064s	passed
seqDef_lower_equals_upper	data()[173]	3.146s	passed
seqDefOfSeq	data()[174]	3.123s	passed
seqSelfDefinitionEQ2	data()[175]	3.076s	passed
indexOfSeqSingleton	data()[176]	3.073s	passed
indexOfSeqConcatFirst	data()[177]	3.051s	passed
indexOfSeqConcatSecond	data()[178]	3.190s	passed
indexOfSeqSub	data()[179]	3.109s	passed
div_zero	data()[17]	3.112s	passed
lenOfArray2seq	data()[180]	3.031s	passed
getAnyOfArray2seq	data()[181]	3.190s	passed
getOfArray2seq	data()[182]	3.220s	passed
getAnyOfNPermInv	data()[183]	3.196s	passed
seqNPermRange	data()[184]	3.224s	passed
seqPermTrans	data()[185]	3.265s	passed
seqPermRefl	data()[186]	3.199s	passed
seqPermSplit	data()[187]	3.127s	passed
seqNPermRight	data()[188]	3.104s	passed
seqPermFromSwap	data()[189]	3.086s	passed
divResZero1	data()[18]	3.298s	passed
seqPermTransAlt0	data()[190]	3.092s	passed
seqPermTransAlt1	data()[191]	3.052s	passed
seqPermTransAlt2	data()[192]	3.078s	passed
seqPermTransAlt3	data()[193]	3.059s	passed
seqPermForall	data()[194]	3.226s	passed
seqPermExists	data()[195]	3.131s	passed
schiffl_lemma_2	data()[196]	21.263s	passed
schiffl_thm_1	data()[197]	3.978s	passed
eqSameSeq	data()[198]	3.212s	passed
divResZero2	data()[19]	3.352s	passed
eqTermCut	data()[1]	3.890s	passed
divResOne1	data()[20]	3.248s	passed
divResOne2	data()[21]	3.222s	passed
div_cancel1	data()[22]	3.324s	passed
div_cancel2	data()[23]	3.198s	passed
divAddMultDenom	data()[24]	3.205s	passed
divMinus	data()[25]	3.195s	passed
divMinusDenom	data()[26]	3.126s	passed
divLeastDPos	data()[27]	3.116s	passed
divLeastDNeg	data()[28]	3.108s	passed
divGreatestDPos	data()[29]	3.148s	passed
equivAllRight	data()[2]	3.526s	passed
divGreatestDNeg	data()[30]	3.143s	passed
divIncreasingPos	data()[31]	3.244s	passed
divIncreasingNeg	data()[32]	3.113s	passed
jdiv_zero	data()[33]	3.093s	passed
jdivPulloutMinusNum	data()[34]	3.221s	passed
jdivPulloutMinusDenom	data()[35]	3.161s	passed
jdiv_uniquePosPos	data()[36]	3.103s	passed
jdiv_uniquePosNeg	data()[37]	3.112s	passed
jdiv_uniqueNegPos	data()[38]	3.109s	passed
jdiv_uniqueNegNeg	data()[39]	3.105s	passed
irrflConcrete1	data()[3]	3.466s	passed
jdivMultDenom1	data()[40]	3.113s	passed
jdivMultDenom2	data()[41]	3.156s	passed
mod_geZero	data()[42]	3.111s	passed
mod_lessDenom	data()[43]	3.085s	passed
jmod_NumPos	data()[44]	3.151s	passed
jmod_NumNeg	data()[45]	3.146s	passed
jmod_geZero	data()[46]	3.051s	passed
jmodNumZero	data()[47]	3.181s	passed
jmod_pulloutminusNum	data()[48]	3.070s	passed
jmod_pulloutminusDenom	data()[49]	3.263s	passed
irrflConcrete2	data()[4]	3.386s	passed
jmodUnique1	data()[50]	3.319s	passed
jmodUnique2	data()[51]	3.328s	passed
intDivRem	data()[52]	3.345s	passed
jmodjmod	data()[53]	3.536s	passed
jmodDivisible	data()[54]	3.408s	passed
jmodDivisibleRep	data()[55]	3.122s	passed
jdivAddMultDenom	data()[56]	3.351s	passed
jmodAltZero	data()[57]	3.148s	passed
jmodAddMultDenomZero	data()[58]	3.091s	passed
polyDiv_zero	data()[59]	3.164s	passed
cancel_gtPos	data()[5]	3.455s	passed
polyMod_ltdivDenom	data()[60]	3.189s	passed
bsum_empty	data()[61]	3.121s	passed
bsum_induction_upper	data()[62]	3.134s	passed
bsum_induction_lower	data()[63]	3.142s	passed
bsum_num_of_bounds	data()[64]	3.069s	passed
bsum_num_of_bounds2	data()[65]	3.200s	passed
bsum_induction_upper2	data()[66]	3.061s	passed
bsum_induction_upper_concrete	data()[67]	3.090s	passed
bsum_induction_upper_concrete_2	data()[68]	3.115s	passed
bsum_induction_upper2_concrete	data()[69]	3.055s	passed
cancel_gtNeg	data()[6]	3.242s	passed
bsum_induction_lower_concrete	data()[70]	3.061s	passed
bsum_induction_lower2	data()[71]	3.033s	passed
bsum_induction_lower2_concrete	data()[72]	3.108s	passed
bsum_positive	data()[73]	3.032s	passed
bsum_upper_bound	data()[74]	3.109s	passed
bsum_lower_bound	data()[75]	3.099s	passed
bsum_positive_lower_bound_element	data()[76]	3.082s	passed
bsum_sub_same_index	data()[77]	3.048s	passed
bsum_less_same_index	data()[78]	3.080s	passed
bsum_equal_except_one_index	data()[79]	3.197s	passed
moduloIntIsInInt	data()[7]	3.273s	passed
bsum_num_of_is_max	data()[80]	3.071s	passed
bsum_num_of_is_max2	data()[81]	3.162s	passed
bsum_num_of_is_max3	data()[82]	3.140s	passed
bsum_num_of_is_max4	data()[83]	3.149s	passed
bsum_num_of_lt_max	data()[84]	3.081s	passed
bsum_num_of_lt_max2	data()[85]	3.230s	passed
bsum_num_of_lt_max3	data()[86]	3.116s	passed
bsum_num_of_lt_max4	data()[87]	3.173s	passed
bsum_num_of_gt0	data()[88]	3.285s	passed
bsum_num_of_gt0_alt	data()[89]	3.253s	passed
moduloLongIsInLong	data()[8]	3.160s	passed
bsum_add_concrete	data()[90]	3.270s	passed
bprod_all_positive	data()[91]	3.208s	passed
bprod_split	data()[92]	3.084s	passed
powConcrete0	data()[93]	3.150s	passed
powConcrete1	data()[94]	3.126s	passed
powSplitFactor	data()[95]	3.092s	passed
powAdd	data()[96]	3.090s	passed
powMono	data()[97]	3.068s	passed
powMonoConcrete	data()[98]	3.139s	passed
powMonoConcreteRight	data()[99]	3.034s	passed
moduloShortIsInShort	data()[9]	3.224s	passed
Standard output

362        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
394        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.72ms 
648        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660        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)

1421       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1423       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1424       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1424       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2852       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7693       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.04s 
7769       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7810       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.7ns 
7825       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7825       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 478.83ns 
7830       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10744      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
10747      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11682      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11705      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.84ms 
11714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11714      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.31ns 
11715      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14333      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
14334      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15218      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15237      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms 
15240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15240      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.81ns 
15242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17913      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
17913      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18699      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18705      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
18708      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18708      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.82ns 
18709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21297      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
21298      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22079      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22090      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
22093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485.93ns 
22095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24690      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
24690      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25546      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.1ms 
25550      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25550      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 476.33ns 
25555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28012      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
28012      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28790      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.05ms 
28793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28793      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.22ns 
28794      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31274      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
31275      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32060      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32063      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 669.14ns 
32067      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32067      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.52ns 
32068      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34435      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
34436      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35222      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35224      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 526.63ns 
35227      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35227      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.42ns 
35228      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37608      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
37609      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38448      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 679.14ns 
38451      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38451      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.92ns 
38452      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40838      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
40839      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41661      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41664      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 508.53ns 
41667      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41667      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.72ns 
41668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44091      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
44092      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44901      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44904      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.34ns 
44907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44908      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 444.53ns 
44909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47305      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
47305      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48136      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.74ms 
48139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48139      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.92ns 
48141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50609      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
50610      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
51448      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.52ms 
51451      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
51452      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.42ns 
51453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
53806      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54764      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 116.63ms 
54767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54767      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.81ns 
54768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57195      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
57196      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58014      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
58016      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58016      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.42ns 
58018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
60450      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
61270      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
61274      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
61276      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
61276      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.61ns 
61277      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63580      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
63580      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
64348      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
64386      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.44ms 
64388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
64388      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.91ns 
64389      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
66882      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
67672      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
67684      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 
67686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
67686      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.71ns 
67687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70215      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
70216      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71036      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
71040      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71040      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 768.64ns 
71045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73506      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
73506      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
74273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
74284      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.24ms 
74286      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
74286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.41ns 
74287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76734      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
76734      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
77495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
77506      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.64ms 
77507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
77507      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
77508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79999      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
80000      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
80805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
80830      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.1ms 
80833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
80834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 635.94ns 
80835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83212      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
83213      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84025      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84028      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
84030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84030      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.91ns 
84031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86390      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
86390      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
87233      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.06ms 
87234      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
87234      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.91ns 
87235      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89602      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
89602      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
90390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
90428      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.8ms 
90431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
90431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.62ns 
90432      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92775      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
92776      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
93527      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
93556      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.47ms 
93557      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
93557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.81ns 
93558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95848      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
95848      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
96665      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
96672      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
96673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
96673      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
96674      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98989      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
98989      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
99768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
99779      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.35ms 
99780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
99780      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.41ns 
99781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
102147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
102918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
102927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.47ms 
102928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
102929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.71ns 
102929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
105263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
106063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
106070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
106071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
106071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.21ns 
106072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
108446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
109307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
109314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
109317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
109317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.82ns 
109318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
111640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
112422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
112429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
112430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
112431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.91ns 
112431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
114740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
115518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
115522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
115526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
115526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
115527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
117984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
118736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
118745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms 
118746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
118747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.71ns 
118747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
121122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
121877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
121906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.07ms 
121908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
121908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.61ns 
121909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
124258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
124994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
125010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ms 
125011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
125011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.51ns 
125012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
127365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
128108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
128121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
128123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
128123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.51ns 
128124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
130461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
131216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
131230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
131232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
131232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.51ns 
131233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
133557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
134324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
134336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
134337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
134337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.61ns 
134338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
136620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
137420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
137449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.33ms 
137450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
137450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
137451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
139817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
140601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
140604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
140606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
140606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
140606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
142930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
143712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
143715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
143716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
143716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.81ns 
143717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
146043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
146794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
146800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
146802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
146802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.81ns 
146803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
149151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
149944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
149951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.81ms 
149952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
149952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
149953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
152282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
153083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
153097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.85ms 
153099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
153099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.01ns 
153100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
155382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
156142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
156148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
156150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
156150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
156150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
158497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
159325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
159329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
159331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
159331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.12ns 
159332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
161620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
162396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
162399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
162401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
162401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.71ns 
162401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
164871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
165660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
165663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
165664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
165664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
165665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
168122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
168919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
168981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.3ms 
168983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
168983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.71ns 
168984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
171429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
172231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
172307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.35ms 
172311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
172311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.92ns 
172312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
174841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
175651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
175654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
175656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
175656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.41ns 
175657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
178298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
179159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
179190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.17ms 
179193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
179193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 465.83ns 
179194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
181789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
182580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
182599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.43ms 
182600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
182600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
182601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
184966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
185719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
185721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 955.86ns 
185722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
185722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
185723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
188118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
188952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
189071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.76ms 
189073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
189073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.91ns 
189074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
191406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
192212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
192220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
192221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
192221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
192222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
194554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
195305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
195311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
195313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
195313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
195313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
197647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
198457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
198475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.77ms 
198476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
198476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.91ns 
198477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
200872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
201652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
201663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms 
201667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
201667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.22ns 
201668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
203968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
204781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
204785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
204787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
204788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.42ns 
204789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
207145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
207916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
207919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
207922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
207922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.42ns 
207923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
210241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
211049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
211062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.16ms 
211063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
211063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.31ns 
211064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
213380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
214115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
214130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.18ms 
214133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
214133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.11ns 
214134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
216562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
217320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
217331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.75ms 
217333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
217333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
217333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
219650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
220389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
220392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
220393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
220393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
220394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
222695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
223477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
223481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
223484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
223484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.41ns 
223485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
225811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
226593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
226597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
226599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
226599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
226599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
228872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
229649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
229652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 873.25ns 
229653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
229653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
229654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
231954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
232712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
232714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 465.03ns 
232715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
232715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
232716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
234993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
235744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
235747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
235748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
235748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
235749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
238092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
238852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
238855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.44ns 
238856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
238857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.51ns 
238857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
241111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
241854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
241886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.87ms 
241888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
241888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.71ns 
241889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
244210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
244974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
244995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.99ms 
244997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
244997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.41ns 
244998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
247311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
248075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
248095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.49ms 
248096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
248096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.61ns 
248097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
250394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
251150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
251177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.75ms 
251178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
251178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
251179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
253448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
254207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
254225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.98ms 
254226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
254226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
254227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
256500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
257271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
257304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.74ms 
257305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
257305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
257306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
259642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
260483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
260502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.22ms 
260503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
260503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
260504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
262818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
263560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
263573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ms 
263574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
263574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
263575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
265970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
266717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
266734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.38ms 
266735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
266735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
266736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
269087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
269862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
269874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 
269875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
269875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
269876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
272229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
272976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
273023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.8ms 
273024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
273024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
273025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
275322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
276090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
276105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.68ms 
276106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
276106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
276107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
278508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
279316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
279334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.72ms 
279336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
279336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
279337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
281659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
282437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
282450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.08ms 
282452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
282452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
282452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
284812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
285610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
285624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.15ms 
285625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
285625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
285625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
288092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
288894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
288908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.51ms 
288910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
288910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
288910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
291363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
292146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
292161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.66ms 
292163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
292163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
292163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
294623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
295426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
295432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
295433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
295433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
295433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
297803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
298627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
298639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.24ms 
298640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
298640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
298641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
300970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
301720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
301723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
301724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
301724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
301726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
304075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
304872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
304874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 475.63ns 
304875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
304876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 654.64ns 
304876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
307207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
307997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
308000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.34ns 
308001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
308002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.71ns 
308002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
310358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
311086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
311092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
311093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
311093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
311094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
313395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
314176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
314181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
314182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
314182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
314183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
316497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
317241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
317249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.79ms 
317251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
317251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
317251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
319574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
320386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
320389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
320390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
320390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
320390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
322630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
323420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
323422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 450.93ns 
323424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
323424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
323424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
325726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
326524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
326529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
326530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
326530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
326531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
328844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
329645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
329647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.13ns 
329650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
329650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
329650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
331939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
332707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
332708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 408.32ns 
332710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
332710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
332710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
334969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
335725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
335726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 416.12ns 
335727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
335728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
335728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
338022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
338768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
338771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
338773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
338773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
338773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
341118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
341876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
341888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.41ms 
341890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
341890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.21ns 
341891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
344282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
345061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
345064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
345065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
345065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
345065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
347346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
348113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
348119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
348120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
348120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
348120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
350467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
351244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
351247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
351248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
351248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
351249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
353540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
354307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
354318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 
354319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
354319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
354320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
356664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
357395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
357398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
357399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
357399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
357400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
359749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
360545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
360549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 983.66ns 
360550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
360550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
360551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
363128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
363881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
363884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
363885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
363885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
363886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
366222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
366969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
366980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
366981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
366981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
366982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
369312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
370055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
370059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 342.82ns 
370061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
370061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
370062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
372405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
373199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
373222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.79ms 
373224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
373224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
373225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
375469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
376241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
376244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
376245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
376245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
376245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
378548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
379345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
379359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.81ms 
379360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
379360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
379361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
381764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
382548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
382563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.96ms 
382564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
382564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
382565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
385019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
385825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
385845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.58ms 
385846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
385847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.11ns 
385847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
388274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
389048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
389050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 538.33ns 
389051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
389051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
389052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
391585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
392368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
392374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
392375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
392375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
392375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
394677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
395428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
395431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
395432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
395432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
395433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
397806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
398569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
398571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 630.44ns 
398573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
398573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
398574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
400825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
401596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
401598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 603.44ns 
401601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
401601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.31ns 
401602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
403948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
404684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
404687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 995.46ns 
404689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
404689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.01ns 
404690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
407011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
407802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
407804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 901.65ns 
407807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
407807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
407807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
410188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
410927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
410934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
410936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
410936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.81ns 
410937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
413256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
414025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
414031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
414033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
414033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
414034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
416331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
417115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
417121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
417124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
417124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
417125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
419468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
420256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
420263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.81ms 
420264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
420264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
420265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
422497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
423293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
423296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
423298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
423298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
423298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
425656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
426431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
426435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
426436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
426436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
426437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
428813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
429600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
429602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 909.15ns 
429603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
429603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
429604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
432167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
432953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
432955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931.75ns 
432957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
432957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
432957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
435268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
436054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
436056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 745.35ns 
436058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
436058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
436058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
438348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
439148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
439156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
439157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
439157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
439158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
441535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
442306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
442309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
442311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
442311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
442311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
444626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
445379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
445387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.82ms 
445388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
445388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
445389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
447735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
448608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
448610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 708.04ns 
448611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
448611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
448612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
450993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
451818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
451820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 508.73ns 
451821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
451821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
451821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
454388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
455306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
455309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
455311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
455311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
455312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
457873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
458692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
458694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 758.35ns 
458695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
458695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
458696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
461075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
461847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
461850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
461851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
461851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
461852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
464229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
465055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
465058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 923.15ns 
465059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
465059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
465059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
467330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
468129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
468132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
468134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
468134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.31ns 
468134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
470460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
471191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
471193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 895.65ns 
471194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
471195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
471195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
473499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
474280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
474287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.91ms 
474288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
474288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
474289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
476594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
477364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
477366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 545.83ns 
477368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
477368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
477368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
479770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
480587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
480593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
480594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
480594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
480595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
482994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
483794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
483797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 850.95ns 
483798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
483798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
483799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
486215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
487036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
487039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 889.55ns 
487040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
487040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
487040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
489400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
490188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
490191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
490192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
490192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
490193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
492536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
493318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
493321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 763.85ns 
493322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
493322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
493323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
495717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
496497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
496500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
496501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
496501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.8ns 
496501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
498791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
499577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
499581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
499583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
499583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.81ns 
499584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
501963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
502746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
502750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
502751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
502751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
502752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
505018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
505795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
505801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
505803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
505803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
505803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
508215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
508977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
508985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.96ms 
508986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
508986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
508987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
511298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
512080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
512085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
512086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
512086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
512087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
514367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
515124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
515130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
515131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
515131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
515132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
517474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
518289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
518299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.73ms 
518301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
518301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
518301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
520595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
521376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
521385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
521386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
521386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
521386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
523733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
524532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
524541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.86ms 
524542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
524542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
524543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
526816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
527602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
527608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
527609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
527609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
527610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
530071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
530846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
530868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.94ms 
530869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
530869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
530870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
533170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
533942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
533964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.16ms 
533965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
533965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
533966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
536235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
537003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
537021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.23ms 
537022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
537022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
537023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
539356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
540136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
540154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.53ms 
540155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
540155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
540156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
542399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
543188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
543206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.47ms 
543207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
543207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
543208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
545456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
546220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
546269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.94ms 
546271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
546271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
546272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
548639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
549416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
549420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
549423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
549423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
549424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
551747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
552479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
552484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
552485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
552485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
552486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
554854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
555627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
555630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
555631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
555632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
555632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
557950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
558742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
558754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.04ms 
558755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
558755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
558756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
561060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
561824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
561830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
561831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
561831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
561832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
564133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
564899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
564902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
564904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
564904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
564904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
567177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
567943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
567954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.47ms 
567955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
567955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
567956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
570341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
571133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
571144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.35ms 
571145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
571145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
571146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
573438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
574240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
574253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.44ms 
574255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
574255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
574256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
576514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
577281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
577283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
577284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
577285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
577285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
579666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
580470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
580474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
580475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
580475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
580476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
582852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
583688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
583693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
583694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
583694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
583695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
586090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
586884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
586889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
586890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
586890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
586891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
589293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
590066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
590113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.48ms 
590115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
590115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.71ns 
590116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
592570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
593361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
593379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.12ms 
593380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
593380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
593381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
595783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
596567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
596578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.21ms 
596579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
596579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
596579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
598871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
599702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
599704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 348.22ns 
599706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
599706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.51ns 
599708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
601979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
602734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
602808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.61ms 
602810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
602810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
602810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
605086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
605862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
605894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.41ms 
605896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
605896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
605897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
608210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
608985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
608986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 224.11ns 
608989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
608989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
608989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
611271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
612037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
612039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 163.71ns 
612040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
612040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
612040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
614336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
615115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
615116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 199.01ns 
615118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
615118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
615118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
617393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
618173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
618175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 343.72ns 
618177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
618177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
618177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
620543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
621328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
621395     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
621402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.94ms 
621403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
621403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
621404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
623714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
624485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
624532     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
624532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.8ms 
624533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
624533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
624535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
626841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
627617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
627618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ns 
627643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
627680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
627696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
627702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
627715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
627716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
627718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
627720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
627725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
627726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
627731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
627733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
627915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
627916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
627917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
627917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
627919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
628084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
628085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
628087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
628088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
628089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
628090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
628270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
628271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
628272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
628273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
628275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
628278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
628465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
628466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
628468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
628468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
628469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
628470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
628479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
628480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
628481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
628482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
628484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
628486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
628495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
628496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
628497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
628498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
628498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
628499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
628652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
628653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
628655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
628766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
628767     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)'' 
628769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
628770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
628771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
628771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
628772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
628774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
628778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
628779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
628780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
628781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
628782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
628889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
628893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
628894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
628895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
628896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
628896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
628898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
629014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
629015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
629016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
629018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
629019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
629019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
629021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
629021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
629127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
629128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
629221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
629225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
629231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
629232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
629236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
629238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
629239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
629239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
629240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
629241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
629250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
629255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
629360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
629360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
629362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
629363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
629364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
629364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
629365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
629365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
629413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
629419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
629512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
629513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
629514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
629515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
629516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
629517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
629642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
629646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
629648     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)'' 
629650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
629651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
629652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
629652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
629652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
629661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
629665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
629666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
629668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
629750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
629751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
629752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
629752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
629753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
629754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
629850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
629851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
629852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
629854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
629854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
629855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
629855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
629856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
629941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
629944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
630034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
630035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
630035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
630039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
630042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
630047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
630174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
630174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
630175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
630176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
630184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
630274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
633678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
633680     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)'' 
633684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
633685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
633685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
633686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
633687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
633694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
633695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
633696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
633697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
633697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
633785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
633789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
633791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
633792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
633795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
633795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
633796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
633890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
633891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
633892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
633893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
633894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
633894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
633895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
633896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
633972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
633973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
634045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
634049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
634053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
634053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
634054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
634055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
634064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
634136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
634136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
634137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
634138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
634209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
634219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
634220     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)'' 
634220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
634222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
634223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
634223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
634224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
634233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
634234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
634235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
634236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
634237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
634321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
634321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
634322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
634323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
634324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
634409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
634413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
634414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
634414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
634415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
634416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
634416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
634506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
634507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
634508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
634509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
634509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
634510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
634510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
634511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
634512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
634512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
634513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
634514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
634514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
634515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
634515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
634594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
634595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
634600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
634670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
634746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
634746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
634747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
634748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
634749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
634749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
634749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
634750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
634750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
634881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
634887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
634976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
634977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
634977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
634978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
634979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
634979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
634980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
634980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
634985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
634985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
635060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
635064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
635069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
635162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
635162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
635163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
635164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
635164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
635164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
635165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
635165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
635215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
635216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
635216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
635217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
635218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
635222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
635227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
635333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
635417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
635418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
635418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
635419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
635581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
635663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
635664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
638552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
638556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
638557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
638558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
638559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
638665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
638666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
638666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
638667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
638668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
638764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
641565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
644622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
644626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
644626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
644627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
644628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
644739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
644739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
644740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
644741     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)' ...' 
644741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
645797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
645797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
645798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
648209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
649052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
649053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
649053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
649060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
649070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
649073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
649075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
649076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
649081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
649081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
649085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
649086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
649088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
649097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
649098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
649100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
649154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
649154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
649155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
649156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
649156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
649229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
649230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
649231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
649232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
649233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
649237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
649237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
649238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
649238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
649239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
649240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
649337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
649338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
649339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
649339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
649340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
649341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
649437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
649438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
649439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
649439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
649440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
649440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
649441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
649442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
649442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
649443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
649444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
649444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
649445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
649445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
649446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
649446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
649447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
649447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
649448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
649451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
649488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
649489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
649542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
649543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
649544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
649545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
649546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
649547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
649600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
649602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
649603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
649604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
649605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
649606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
649607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
649661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
649664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
649668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
649725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
649775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
649775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.21ns 
649776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
652172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
652970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
652985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.04ms