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

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

Test	Method name	Duration	Result
powPositive	data()[100]	3.053s	passed
powPositiveConcrete	data()[101]	3.037s	passed
powGeq1Concrete	data()[102]	3.027s	passed
pow2InIntLower	data()[103]	3.052s	passed
pow2InIntUpper	data()[104]	3.036s	passed
logSelfConcrete	data()[105]	3.057s	passed
log1Concrete	data()[106]	3.031s	passed
logProduct	data()[107]	3.049s	passed
logTimesBaseConcrete	data()[108]	3.046s	passed
logProdIdentity	data()[109]	3.089s	passed
moduloByteIsInByte	data()[10]	3.115s	passed
logProdIdentityConcrete	data()[110]	3.049s	passed
logPowIdentity	data()[111]	3.038s	passed
logPowIdentityConcrete	data()[112]	3.110s	passed
logPositive	data()[113]	3.058s	passed
logPositiveConcrete	data()[114]	3.038s	passed
logMono	data()[115]	3.046s	passed
logMonoConcrete	data()[116]	3.045s	passed
powLogLess	data()[117]	3.042s	passed
powLogMore2	data()[118]	3.051s	passed
logLessThanPow	data()[119]	3.061s	passed
moduloCharIsInChar	data()[11]	3.131s	passed
logLessThanPowConcrete	data()[120]	3.054s	passed
logSqueeze	data()[121]	3.048s	passed
ifthenelse_equals	data()[122]	3.049s	passed
ifthenelse_equals_1	data()[123]	3.056s	passed
ifthenelse_equals_2	data()[124]	3.032s	passed
disjointWithSingleton1	data()[125]	3.045s	passed
disjointWithSingleton2	data()[126]	3.050s	passed
disjointArrayRanges	data()[127]	3.037s	passed
disjointArrayRangeAllFields1	data()[128]	3.058s	passed
disjointArrayRangeAllFields2	data()[129]	3.036s	passed
div_unique1	data()[12]	3.118s	passed
seqSelfDefinition	data()[130]	3.059s	passed
seqOutsideValue	data()[131]	3.036s	passed
castedGetAny	data()[132]	3.051s	passed
seqGetAlphaCast	data()[133]	3.138s	passed
getOfSeqSingleton	data()[134]	3.100s	passed
getOfSeqSingletonConcrete	data()[135]	3.051s	passed
getOfSeqConcat	data()[136]	3.045s	passed
getOfSeqSub	data()[137]	3.061s	passed
getOfSeqReverse	data()[138]	3.041s	passed
lenOfSeqEmpty	data()[139]	3.067s	passed
div_unique2	data()[13]	3.103s	passed
lenOfSeqSingleton	data()[140]	3.051s	passed
lenOfSeqConcat	data()[141]	3.033s	passed
lenOfSeqSub	data()[142]	3.045s	passed
lenOfSeqReverse	data()[143]	3.042s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.031s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.044s	passed
getOfSeqSingletonEQ	data()[146]	3.045s	passed
getOfSeqConcatEQ	data()[147]	3.030s	passed
getOfSeqSubEQ	data()[148]	3.047s	passed
getOfSeqReverseEQ	data()[149]	3.045s	passed
div_exists	data()[14]	3.272s	passed
lenOfSeqEmptyEQ	data()[150]	3.046s	passed
lenOfSeqSingletonEQ	data()[151]	3.030s	passed
lenOfSeqConcatEQ	data()[152]	3.049s	passed
lenOfSeqSubEQ	data()[153]	3.044s	passed
lenOfSeqReverseEQ	data()[154]	3.046s	passed
getOfSeqDefEQ	data()[155]	3.040s	passed
lenOfSeqDefEQ	data()[156]	3.027s	passed
seqConcatWithSeqEmpty1	data()[157]	3.048s	passed
seqConcatWithSeqEmpty2	data()[158]	3.048s	passed
seqReverseOfSeqEmpty	data()[159]	3.059s	passed
div_one	data()[15]	3.121s	passed
subSeqComplete	data()[160]	3.048s	passed
subSeqTailR	data()[161]	3.053s	passed
subSeqTailL	data()[162]	3.064s	passed
subSeqTailEQR	data()[163]	3.054s	passed
subSeqTailEQL	data()[164]	3.074s	passed
seqDef_split	data()[165]	3.044s	passed
seqDef_induction_upper	data()[166]	3.059s	passed
seqDef_induction_upper_concrete	data()[167]	3.060s	passed
seqDef_induction_lower	data()[168]	3.078s	passed
seqDef_induction_lower_concrete	data()[169]	3.055s	passed
jdiv_one	data()[16]	3.092s	passed
seqDef_split_in_three	data()[170]	3.117s	passed
seqDef_empty	data()[171]	3.054s	passed
seqDef_one_summand	data()[172]	3.052s	passed
seqDef_lower_equals_upper	data()[173]	3.043s	passed
seqDefOfSeq	data()[174]	3.055s	passed
seqSelfDefinitionEQ2	data()[175]	3.049s	passed
indexOfSeqSingleton	data()[176]	3.048s	passed
indexOfSeqConcatFirst	data()[177]	3.068s	passed
indexOfSeqConcatSecond	data()[178]	3.069s	passed
indexOfSeqSub	data()[179]	3.054s	passed
div_zero	data()[17]	3.092s	passed
lenOfArray2seq	data()[180]	3.044s	passed
getAnyOfArray2seq	data()[181]	3.108s	passed
getOfArray2seq	data()[182]	3.047s	passed
getAnyOfNPermInv	data()[183]	3.064s	passed
seqNPermRange	data()[184]	3.161s	passed
seqPermTrans	data()[185]	3.150s	passed
seqPermRefl	data()[186]	3.054s	passed
seqPermSplit	data()[187]	3.046s	passed
seqNPermRight	data()[188]	3.121s	passed
seqPermFromSwap	data()[189]	3.100s	passed
divResZero1	data()[18]	3.114s	passed
seqPermTransAlt0	data()[190]	3.049s	passed
seqPermTransAlt1	data()[191]	3.041s	passed
seqPermTransAlt2	data()[192]	3.059s	passed
seqPermTransAlt3	data()[193]	3.043s	passed
seqPermForall	data()[194]	3.133s	passed
seqPermExists	data()[195]	3.113s	passed
schiffl_lemma_2	data()[196]	21.000s	passed
schiffl_thm_1	data()[197]	3.897s	passed
eqSameSeq	data()[198]	3.176s	passed
divResZero2	data()[19]	3.071s	passed
eqTermCut	data()[1]	3.701s	passed
divResOne1	data()[20]	3.071s	passed
divResOne2	data()[21]	3.094s	passed
div_cancel1	data()[22]	3.112s	passed
div_cancel2	data()[23]	3.080s	passed
divAddMultDenom	data()[24]	3.100s	passed
divMinus	data()[25]	3.117s	passed
divMinusDenom	data()[26]	3.090s	passed
divLeastDPos	data()[27]	3.049s	passed
divLeastDNeg	data()[28]	3.078s	passed
divGreatestDPos	data()[29]	3.068s	passed
equivAllRight	data()[2]	3.393s	passed
divGreatestDNeg	data()[30]	3.068s	passed
divIncreasingPos	data()[31]	3.079s	passed
divIncreasingNeg	data()[32]	3.068s	passed
jdiv_zero	data()[33]	3.047s	passed
jdivPulloutMinusNum	data()[34]	3.046s	passed
jdivPulloutMinusDenom	data()[35]	3.172s	passed
jdiv_uniquePosPos	data()[36]	3.081s	passed
jdiv_uniquePosNeg	data()[37]	3.059s	passed
jdiv_uniqueNegPos	data()[38]	3.058s	passed
jdiv_uniqueNegNeg	data()[39]	3.063s	passed
irrflConcrete1	data()[3]	3.314s	passed
jdivMultDenom1	data()[40]	3.069s	passed
jdivMultDenom2	data()[41]	3.040s	passed
mod_geZero	data()[42]	3.061s	passed
mod_lessDenom	data()[43]	3.060s	passed
jmod_NumPos	data()[44]	3.059s	passed
jmod_NumNeg	data()[45]	3.074s	passed
jmod_geZero	data()[46]	3.043s	passed
jmodNumZero	data()[47]	3.057s	passed
jmod_pulloutminusNum	data()[48]	3.049s	passed
jmod_pulloutminusDenom	data()[49]	3.056s	passed
irrflConcrete2	data()[4]	3.188s	passed
jmodUnique1	data()[50]	3.093s	passed
jmodUnique2	data()[51]	3.103s	passed
intDivRem	data()[52]	3.054s	passed
jmodjmod	data()[53]	3.069s	passed
jmodDivisible	data()[54]	3.051s	passed
jmodDivisibleRep	data()[55]	3.042s	passed
jdivAddMultDenom	data()[56]	3.148s	passed
jmodAltZero	data()[57]	3.051s	passed
jmodAddMultDenomZero	data()[58]	3.039s	passed
polyDiv_zero	data()[59]	3.081s	passed
cancel_gtPos	data()[5]	3.222s	passed
polyMod_ltdivDenom	data()[60]	3.050s	passed
bsum_empty	data()[61]	3.021s	passed
bsum_induction_upper	data()[62]	3.050s	passed
bsum_induction_lower	data()[63]	3.047s	passed
bsum_num_of_bounds	data()[64]	3.042s	passed
bsum_num_of_bounds2	data()[65]	3.051s	passed
bsum_induction_upper2	data()[66]	3.044s	passed
bsum_induction_upper_concrete	data()[67]	3.023s	passed
bsum_induction_upper_concrete_2	data()[68]	3.027s	passed
bsum_induction_upper2_concrete	data()[69]	3.051s	passed
cancel_gtNeg	data()[6]	3.209s	passed
bsum_induction_lower_concrete	data()[70]	3.032s	passed
bsum_induction_lower2	data()[71]	3.025s	passed
bsum_induction_lower2_concrete	data()[72]	3.022s	passed
bsum_positive	data()[73]	3.085s	passed
bsum_upper_bound	data()[74]	3.065s	passed
bsum_lower_bound	data()[75]	3.051s	passed
bsum_positive_lower_bound_element	data()[76]	3.085s	passed
bsum_sub_same_index	data()[77]	3.055s	passed
bsum_less_same_index	data()[78]	3.070s	passed
bsum_equal_except_one_index	data()[79]	3.090s	passed
moduloIntIsInInt	data()[7]	3.135s	passed
bsum_num_of_is_max	data()[80]	3.036s	passed
bsum_num_of_is_max2	data()[81]	3.044s	passed
bsum_num_of_is_max3	data()[82]	3.041s	passed
bsum_num_of_is_max4	data()[83]	3.062s	passed
bsum_num_of_lt_max	data()[84]	3.043s	passed
bsum_num_of_lt_max2	data()[85]	3.041s	passed
bsum_num_of_lt_max3	data()[86]	3.060s	passed
bsum_num_of_lt_max4	data()[87]	3.047s	passed
bsum_num_of_gt0	data()[88]	3.042s	passed
bsum_num_of_gt0_alt	data()[89]	3.077s	passed
moduloLongIsInLong	data()[8]	3.137s	passed
bsum_add_concrete	data()[90]	3.045s	passed
bprod_all_positive	data()[91]	3.041s	passed
bprod_split	data()[92]	3.031s	passed
powConcrete0	data()[93]	3.044s	passed
powConcrete1	data()[94]	3.033s	passed
powSplitFactor	data()[95]	3.029s	passed
powAdd	data()[96]	3.051s	passed
powMono	data()[97]	3.038s	passed
powMonoConcrete	data()[98]	3.030s	passed
powMonoConcreteRight	data()[99]	3.028s	passed
moduloShortIsInShort	data()[9]	3.169s	passed
Standard output

598        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
621        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.53ms 
808        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
832        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)

1735       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1737       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1738       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1738       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3191       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8048       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.24s 
8122       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8155       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.5ns 
8170       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8170       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 522ns 
8176       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10970      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
10972      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11861      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.62ms 
11873      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11874      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.2ns 
11875      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
14424      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15264      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
15267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15267      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.3ns 
15269      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17746      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
17747      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18578      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
18580      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18580      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.2ns 
18582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20983      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
20984      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21766      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
21769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21769      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.4ns 
21770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
24141      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24986      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.33ms 
24995      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24995      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379ns 
24998      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27381      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
27381      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28201      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.87ms 
28204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28204      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336ns 
28205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30581      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
30581      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31337      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 582.3ns 
31339      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.4ns 
31340      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33684      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
33684      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34470      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34474      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 718.6ns 
34476      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34476      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.8ns 
34477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36865      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
36865      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37643      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 518.9ns 
37645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37645      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.2ns 
37646      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
39968      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40755      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40758      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 567.3ns 
40760      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40761      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.8ns 
40762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43101      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
43101      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
43884      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
43888      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.69ns 
43892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
43892      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.1ns 
43895      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
46211      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
46974      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47008      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.8ms 
47013      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47013      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.4ns 
47015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49324      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
49324      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50113      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.48ms 
50115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50116      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.3ns 
50117      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52461      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
52461      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
53385      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 161.65ms 
53388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
53388      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129ns 
53389      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55725      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
55725      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
56502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
56507      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms 
56509      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
56510      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.5ns 
56511      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58825      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
58827      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
59596      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
59599      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
59601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
59601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
59602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61918      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
61919      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
62657      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
62691      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.96ms 
62692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
62693      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.5ns 
62693      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65036      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
65036      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
65794      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
65805      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.72ms 
65807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
65807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
65808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68107      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
68108      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
68866      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
68877      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ms 
68878      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
68878      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns 
68879      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71176      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
71176      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
71936      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
71947      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 
71949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
71949      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
71950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
74269      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
75030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
75041      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
75044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
75044      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.6ns 
75045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77378      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
77379      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
78136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
78153      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ms 
78155      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
78155      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.1ns 
78163      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80473      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
80473      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
81230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
81234      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
81236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
81236      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.1ns 
81237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83558      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
83559      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
84304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
84333      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.57ms 
84335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
84335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.4ns 
84336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
86650      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
87407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
87450      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.5ms 
87451      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
87452      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.1ns 
87453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89756      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
89756      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
90511      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
90540      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.53ms 
90542      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
90542      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.5ns 
90543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92828      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
92828      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
93582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
93589      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.46ms 
93590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
93590      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
93591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95901      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
95901      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
96655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
96667      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.53ms 
96670      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
96670      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.3ns 
96671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98965      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
98965      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
99726      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
99735      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.74ms 
99736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
99736      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
99737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
102027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
102798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
102804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
102805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
102805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
102806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
105137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
105876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
105882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
105884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
105885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.7ns 
105886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
108192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
108945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
108951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.55ms 
108952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
108952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
108953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
111239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
111994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
111997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
111998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
111999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
111999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
114305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
115036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
115044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
115045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
115045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
115046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
117385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
118143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
118212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.04ms 
118217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
118218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.9ns 
118232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
120530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
121283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
121297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
121300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
121300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256ns 
121301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
123585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
124343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
124356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.27ms 
124357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
124357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
124358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
126667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
127399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
127415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.82ms 
127416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
127416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
127417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
129713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
130465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
130477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 
130479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
130479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
130479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
132764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
133517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
133545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.31ms 
133548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
133548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.3ns 
133548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
135852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
136584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
136586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
136587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
136587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
136588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
138892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
139644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
139647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
139648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
139648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
139649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
141949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
142701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
142707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
142708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
142708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
142709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
144989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
145760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
145767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 
145768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
145768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
145769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
148071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
148825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
148840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.77ms 
148841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
148841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.2ns 
148842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
151124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
151874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
151883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.57ms 
151887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
151887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.8ns 
151887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
154170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
154936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
154941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
154944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
154944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.2ns 
154945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
157258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
157988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
157991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
157992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
157992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
157993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
160290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
161043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
161046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
161047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
161047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
161048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
163329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
164089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
164139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.8ms 
164140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
164140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
164141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
166450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
167183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
167242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.3ms 
167244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
167244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.5ns 
167245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
169544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
170294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
170296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
170298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
170298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
170298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
172589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
173339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
173365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.97ms 
173366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
173367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
173367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
175647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
176398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
176417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.86ms 
176418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
176419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.5ns 
176419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
178721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
179453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
179455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 892.09ns 
179462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
179464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.49ms 
179465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
181764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
182515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
182608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.28ms 
182609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
182609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
182610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
184901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
185651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
185659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.87ms 
185660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
185660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
185661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
187962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
188693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
188699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
188700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
188700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
188700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
191005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
191754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
191780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.86ms 
191782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
191782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
191782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
194063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
194818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
194828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
194830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
194830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
194831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
197115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
197848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
197851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
197852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
197852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
197853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
200147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
200897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
200900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
200901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
200902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
200902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
203185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
203934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
203947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.34ms 
203949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
203949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
203949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
206227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
206979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
206990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.15ms 
206991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
206991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
206991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
209300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
210030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
210041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.16ms 
210042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
210043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.2ns 
210043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
212335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
213082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
213085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 852.79ns 
213086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
213086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
213087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
215357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
216105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
216108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
216109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
216109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
216109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
218401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
219130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
219134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
219135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
219135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
219136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
221434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
222183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
222185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.6ns 
222186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
222186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
222187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
224466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
225215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
225217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 423.8ns 
225219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
225219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
225219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
227491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
228239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
228242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
228243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
228243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
228244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
230533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
231262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
231264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 566.6ns 
231265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
231265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
231266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
233560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
234315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
234349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.3ms 
234351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
234351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.2ns 
234352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
236628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
237383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
237414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.64ms 
237416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
237416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.4ns 
237417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
239713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
240443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
240465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.17ms 
240466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
240466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
240467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
242769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
243519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
243550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.62ms 
243552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
243552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
243552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
245833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
246586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
246605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.18ms 
246607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
246607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.8ns 
246608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
248883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
249633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
249675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.81ms 
249677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
249677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
249677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
251999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
252745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
252765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.04ms 
252767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
252767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
252767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
255040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
255789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
255801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
255803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
255803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
255803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
258079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
258830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
258846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.24ms 
258847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
258848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175ns 
258848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
261143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
261874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
261886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
261887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
261887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
261888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
264185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
264932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
264948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.92ms 
264949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
264949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
264950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
267228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
267976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
267991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
267992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
267992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
267993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
270283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
271017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
271032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.19ms 
271034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
271034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
271035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
273330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
274078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
274092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.55ms 
274093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
274093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
274094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
276373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
277126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
277139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.41ms 
277140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
277140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
277141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
279418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
280167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
280182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.78ms 
280183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
280183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
280184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
282483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
283236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
283258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.23ms 
283259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
283259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
283260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
285544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
286294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
286304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ms 
286306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
286307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.6ns 
286307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
288585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
289335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
289346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.08ms 
289347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
289347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
289348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
291643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
292373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
292376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
292377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
292378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
292378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
294669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
295419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
295421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 500.8ns 
295422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
295422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.7ns 
295422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
297700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
298451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
298453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 656.2ns 
298454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
298454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
298455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
300728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
301478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
301482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
301484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
301484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
301484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
303777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
304528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
304533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
304534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
304534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
304535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
306815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
307563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
307572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.68ms 
307573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
307573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
307574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
309848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
310598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
310601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
310602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
310602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.6ns 
310603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
312895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
313627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
313629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 433.6ns 
313630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
313630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
313631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
315926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
316677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
316682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
316684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
316684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.4ns 
316684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
318967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
319717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
319719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 517.3ns 
319720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
319720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.5ns 
319721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
322016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
322745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
322746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 438.5ns 
322748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
322748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
322748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
325047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
325796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
325798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 470.1ns 
325799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
325799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
325800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
328079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
328831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
328835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
328836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
328836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
328836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
331119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
331885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
331891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
331892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
331892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
331893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
334190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
334919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
334922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
334923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
334923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
334924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
337218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
337966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
337971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
337972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
337972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.4ns 
337973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
340255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
341009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
341017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.63ms 
341018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
341018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
341019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
343365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
344096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
344107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 
344108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
344108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
344109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
346404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
347153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
347156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
347157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
347157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
347157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
349435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
350186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
350193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
350194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
350195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
350195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
352559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
353300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
353303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
353305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
353305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
353305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
355600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
356349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
356361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.46ms 
356362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
356362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
356363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
358648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
359396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
359399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 265.6ns 
359401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
359401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
359402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
361692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
362422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
362445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.8ms 
362447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
362447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
362447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
364739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
365488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
365490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
365491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
365491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
365492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
367769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
368519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
368533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.23ms 
368534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
368534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
368535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
370837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
371570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
371583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.42ms 
371584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
371584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
371585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
373874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
374627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
374644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms 
374645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
374645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
374646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
376945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
377696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
377698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 475.4ns 
377699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
377699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
377700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
379994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
380742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
380747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
380748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
380748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
380748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
383032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
383792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
383795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
383796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
383796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
383797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
386096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
386850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
386852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.7ns 
386853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
386853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.1ns 
386853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
389131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
389882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
389884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 654ns 
389885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
389885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
389886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
392190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
392925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
392928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.19ns 
392929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
392929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
392930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
395222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
395976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
395978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 926.19ns 
395979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
395980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
395980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
398274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
399009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
399015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 
399017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
399017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.8ns 
399018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
401313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
402068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
402074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.98ms 
402075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
402075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
402075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
404369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
405103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
405109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.96ms 
405110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
405110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
405111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
407403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
408162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
408169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
408170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
408170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
408170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
410459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
411201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
411205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
411206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
411206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
411207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
413495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
414252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
414255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
414256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
414257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
414257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
416606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
417392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
417394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 669.7ns 
417395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
417395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
417395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
419731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
420491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
420493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 801.5ns 
420494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
420494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
420495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
422784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
423542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
423544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 693.2ns 
423545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
423545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
423546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
425823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
426582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
426590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.61ms 
426591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
426591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
426591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
428885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
429647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
429650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
429652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
429652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.8ns 
429653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
431945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
432687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
432692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
432693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
432693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
432694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
434997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
435756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
435758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 661.39ns 
435760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
435760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
435760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
438048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
438808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
438810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 524.3ns 
438811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
438811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
438811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
441080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
441840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
441842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
441843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
441843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
441844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
444127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
444885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
444887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.88ns 
444888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
444889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
444889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
447170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
447928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
447930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 887.39ns 
447931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
447931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
447932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
450200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
450958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
450960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 806.59ns 
450961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
450961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
450962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
453242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
454001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
454004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
454006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
454006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
454006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
456288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
457047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
457049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 654.8ns 
457051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
457051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
457051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
459332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
460072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
460080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.99ms 
460081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
460081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
460082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
462365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
463125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
463126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 432ns 
463127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
463127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
463128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
465407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
466167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
466172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
466173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
466173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
466173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
468456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
469216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
469218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 656.69ns 
469219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
469219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.7ns 
469220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
471503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
472246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
472248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570ns 
472249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
472249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
472249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
474534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
475293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
475296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
475297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
475297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns 
475298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
477578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
478338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
478341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 839.49ns 
478342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
478342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
478342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
480626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
481384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
481387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
481388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
481388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
481389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
483666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
484424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
484427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 899.09ns 
484428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
484428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
484428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
486692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
487450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
487453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
487454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
487454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
487455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
489734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
490495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
490501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms 
490503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
490503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
490503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
492784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
493542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
493549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
493550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
493550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
493551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
495836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
496603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
496608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
496610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
496610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
496610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
498893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
499651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
499656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
499657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
499657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
499658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
501941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
502700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
502709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.06ms 
502710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
502710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
502711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
505004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
505764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
505774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
505775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
505775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
505775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
508058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
508818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
508827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.32ms 
508830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
508830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.1ns 
508830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
511123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
511864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
511902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.07ms 
511903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
511903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
511904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
514187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
514929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
514947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.97ms 
514948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
514948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
514948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
517246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
517986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
518006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.23ms 
518007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
518007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
518008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
520287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
521048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
521065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.54ms 
521067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
521067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
521067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
523369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
524126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
524143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms 
524144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
524144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
524145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
526441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
527182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
527199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.27ms 
527200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
527200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
527201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
529501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
530245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
530315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.61ms 
530316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
530316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
530317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
532601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
533361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
533369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
533371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
533371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
533371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
535659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
536417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
536421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
536422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
536423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
536423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
538702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
539461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
539464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
539465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
539465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.4ns 
539466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
541748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
542508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
542519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.91ms 
542520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
542520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
542521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
544803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
545563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
545569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
545570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
545570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
545573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
547855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
548614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
548616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
548617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
548618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
548618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
550897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
551675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
551684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.93ms 
551685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
551685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
551686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
553984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
554744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
554753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
554754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
554754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
554755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
557036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
557796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
557807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.46ms 
557808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
557809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
557809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
560089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
560849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
560852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.69ns 
560853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
560853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
560854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
563197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
563957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
563960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
563961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
563961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
563961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
566240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
567001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
567006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
567007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
567007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
567008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
569290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
570067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
570071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
570072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
570072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.4ns 
570073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
572406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
573193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
573232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.02ms 
573233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
573233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
573234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
575591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
576356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
576381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.59ms 
576382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
576383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
576383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
578666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
579426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
579435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.73ms 
579436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
579436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
579437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
581718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
582480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
582481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 132.8ns 
582483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
582483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.9ns 
582484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
584771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
585531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
585602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.73ms 
585603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
585603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
585604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
587909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
588672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
588703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.25ms 
588704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
588704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
588705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
590987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
591750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
591752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 160.4ns 
591754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
591754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
591755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
594032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
594792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
594793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 184.9ns 
594795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
594795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
594795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
597092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
597851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
597852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 178.2ns 
597853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
597853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.8ns 
597854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
600133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
600894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
600895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 279.4ns 
600896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
600896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
600897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
603170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
603943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
604021     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
604028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.4ms 
604030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
604030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.2ns 
604031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
606336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
607096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
607141     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
607142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.37ms 
607143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
607143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
607144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
609430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
610198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
610199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ns 
610223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
610258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
610269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
610273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
610281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
610282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
610283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
610284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
610288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
610289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
610291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
610292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
610482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
610483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
610484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
610485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
610487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
610621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
610622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
610625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
610626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
610628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
610629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
610785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
610787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
610788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
610789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
610790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
610793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
610915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
610917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
610918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
610919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
610920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
610921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
610929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
610930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
610931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
610932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
610934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
610936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
610945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
610946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
610947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
610948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
610948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
610949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
611102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
611103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
611104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
611223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
611224     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)'' 
611226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
611228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
611228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
611229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
611230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
611232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
611236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
611237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
611238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
611239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
611240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
611346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
611351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
611352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
611353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
611353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
611354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
611356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
611477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
611478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
611479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
611480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
611481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
611481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
611483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
611483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
611579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
611581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
611667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
611671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
611676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
611677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
611678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
611680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
611680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
611681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
611681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
611682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
611690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
611695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
611818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
611819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
611821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
611822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
611823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
611824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
611826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
611826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
611888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
611896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
611994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
611995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
611997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
611998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
612000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
612000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
612132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
612136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
612138     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)'' 
612140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
612141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
612142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
612142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
612143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
612151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
612156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
612157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
612158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
612252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
612253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
612254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
612255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
612255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
612256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
612362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
612363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
612364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
612366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
612366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
612367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
612368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
612368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
612452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
612453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
612525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
612525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
612526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
612530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
612534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
612538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
612655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
612656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
612657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
612658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
612667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
612758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
616157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
616158     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)'' 
616162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
616168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
616169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
616169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
616171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
616178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
616179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
616180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
616181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
616182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
616270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
616273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
616274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
616275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
616276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
616276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
616277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
616366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
616367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
616368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
616370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
616371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
616372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
616372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
616373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
616445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
616446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
616516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
616520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
616524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
616525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
616526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
616527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
616536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
616611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
616612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
616613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
616614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
616681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
616692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
616693     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)'' 
616693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
616695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
616695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
616695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
616696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
616706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
616706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
616707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
616708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
616709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
616833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
616835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
616837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
616838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
616839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
616932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
616937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
616937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
616938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
616939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
616940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
616940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
617033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
617034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
617035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
617036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
617037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
617038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
617038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
617039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
617039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
617040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
617042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
617043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
617043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
617044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
617044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
617127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
617128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
617133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
617206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
617284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
617285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
617285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
617286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
617287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
617287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
617287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
617288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
617288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
617369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
617375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
617461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
617462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
617463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
617464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
617465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
617465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
617465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
617466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
617470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
617471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
617546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
617551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
617556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
617649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
617649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
617650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
617651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
617651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
617651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
617652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
617652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
617703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
617703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
617704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
617704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
617705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
617710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
617715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
617824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
617907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
617908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
617908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
617909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
618065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
618148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
618148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
620968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
620972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
620973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
620974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
620975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
621082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
621083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
621084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
621084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
621085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
621184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
623951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
626939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
626943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
626944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
626944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
626945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
627052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
627052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
627053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
627054     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)' ...' 
627055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
628143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
628143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
628144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
630605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
631388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
631390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ns 
631390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
631396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
631404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
631407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
631409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
631411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
631415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
631415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
631419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
631419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
631422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
631430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
631430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
631432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
631474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
631475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
631475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
631476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
631476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
631544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
631544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
631545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
631546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
631547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
631550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
631551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
631551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
631552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
631553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
631553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
631639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
631639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
631640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
631640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
631642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
631642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
631728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
631728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
631729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
631729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
631730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
631731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
631731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
631732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
631732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
631733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
631733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
631734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
631734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
631735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
631735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
631736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
631736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
631737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
631737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
631740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
631779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
631780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
631842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
631843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
631844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
631845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
631846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
631846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
631893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
631895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
631896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
631897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
631898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
631899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
631900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
631940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
631942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
631945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
631991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
632040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
632040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.2ns 
632041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
634389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
635200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
635214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.49ms