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

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

Test	Method name	Duration	Result
powPositive	data()[100]	3.932s	passed
powPositiveConcrete	data()[101]	3.802s	passed
powGeq1Concrete	data()[102]	3.831s	passed
pow2InIntLower	data()[103]	3.781s	passed
pow2InIntUpper	data()[104]	3.909s	passed
logSelfConcrete	data()[105]	3.954s	passed
log1Concrete	data()[106]	3.847s	passed
logProduct	data()[107]	3.815s	passed
logTimesBaseConcrete	data()[108]	3.822s	passed
logProdIdentity	data()[109]	3.801s	passed
moduloByteIsInByte	data()[10]	4.137s	passed
logProdIdentityConcrete	data()[110]	3.948s	passed
logPowIdentity	data()[111]	3.822s	passed
logPowIdentityConcrete	data()[112]	3.852s	passed
logPositive	data()[113]	3.970s	passed
logPositiveConcrete	data()[114]	3.850s	passed
logMono	data()[115]	3.852s	passed
logMonoConcrete	data()[116]	3.804s	passed
powLogLess	data()[117]	3.835s	passed
powLogMore2	data()[118]	3.892s	passed
logLessThanPow	data()[119]	3.852s	passed
moduloCharIsInChar	data()[11]	3.907s	passed
logLessThanPowConcrete	data()[120]	3.837s	passed
logSqueeze	data()[121]	3.888s	passed
ifthenelse_equals	data()[122]	3.807s	passed
ifthenelse_equals_1	data()[123]	3.849s	passed
ifthenelse_equals_2	data()[124]	3.823s	passed
disjointWithSingleton1	data()[125]	3.932s	passed
disjointWithSingleton2	data()[126]	3.880s	passed
disjointArrayRanges	data()[127]	4.009s	passed
disjointArrayRangeAllFields1	data()[128]	3.985s	passed
disjointArrayRangeAllFields2	data()[129]	3.874s	passed
div_unique1	data()[12]	3.973s	passed
seqSelfDefinition	data()[130]	3.923s	passed
seqOutsideValue	data()[131]	3.855s	passed
castedGetAny	data()[132]	3.901s	passed
seqGetAlphaCast	data()[133]	3.988s	passed
getOfSeqSingleton	data()[134]	3.852s	passed
getOfSeqSingletonConcrete	data()[135]	3.806s	passed
getOfSeqConcat	data()[136]	3.942s	passed
getOfSeqSub	data()[137]	3.914s	passed
getOfSeqReverse	data()[138]	4.028s	passed
lenOfSeqEmpty	data()[139]	3.833s	passed
div_unique2	data()[13]	4.002s	passed
lenOfSeqSingleton	data()[140]	3.933s	passed
lenOfSeqConcat	data()[141]	3.881s	passed
lenOfSeqSub	data()[142]	3.850s	passed
lenOfSeqReverse	data()[143]	3.937s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.826s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.897s	passed
getOfSeqSingletonEQ	data()[146]	3.828s	passed
getOfSeqConcatEQ	data()[147]	3.849s	passed
getOfSeqSubEQ	data()[148]	3.799s	passed
getOfSeqReverseEQ	data()[149]	3.872s	passed
div_exists	data()[14]	4.188s	passed
lenOfSeqEmptyEQ	data()[150]	3.840s	passed
lenOfSeqSingletonEQ	data()[151]	3.805s	passed
lenOfSeqConcatEQ	data()[152]	3.915s	passed
lenOfSeqSubEQ	data()[153]	3.978s	passed
lenOfSeqReverseEQ	data()[154]	3.800s	passed
getOfSeqDefEQ	data()[155]	3.866s	passed
lenOfSeqDefEQ	data()[156]	3.928s	passed
seqConcatWithSeqEmpty1	data()[157]	3.936s	passed
seqConcatWithSeqEmpty2	data()[158]	3.903s	passed
seqReverseOfSeqEmpty	data()[159]	3.887s	passed
div_one	data()[15]	3.972s	passed
subSeqComplete	data()[160]	3.849s	passed
subSeqTailR	data()[161]	4.006s	passed
subSeqTailL	data()[162]	3.842s	passed
subSeqTailEQR	data()[163]	4.013s	passed
subSeqTailEQL	data()[164]	3.933s	passed
seqDef_split	data()[165]	3.895s	passed
seqDef_induction_upper	data()[166]	3.918s	passed
seqDef_induction_upper_concrete	data()[167]	3.865s	passed
seqDef_induction_lower	data()[168]	4.046s	passed
seqDef_induction_lower_concrete	data()[169]	3.977s	passed
jdiv_one	data()[16]	3.877s	passed
seqDef_split_in_three	data()[170]	4.137s	passed
seqDef_empty	data()[171]	3.950s	passed
seqDef_one_summand	data()[172]	3.916s	passed
seqDef_lower_equals_upper	data()[173]	3.925s	passed
seqDefOfSeq	data()[174]	3.873s	passed
seqSelfDefinitionEQ2	data()[175]	3.865s	passed
indexOfSeqSingleton	data()[176]	3.946s	passed
indexOfSeqConcatFirst	data()[177]	3.949s	passed
indexOfSeqConcatSecond	data()[178]	3.917s	passed
indexOfSeqSub	data()[179]	3.899s	passed
div_zero	data()[17]	3.892s	passed
lenOfArray2seq	data()[180]	4.102s	passed
getAnyOfArray2seq	data()[181]	3.887s	passed
getOfArray2seq	data()[182]	3.853s	passed
getAnyOfNPermInv	data()[183]	3.855s	passed
seqNPermRange	data()[184]	3.985s	passed
seqPermTrans	data()[185]	3.858s	passed
seqPermRefl	data()[186]	3.886s	passed
seqPermSplit	data()[187]	3.854s	passed
seqNPermRight	data()[188]	4.120s	passed
seqPermFromSwap	data()[189]	4.025s	passed
divResZero1	data()[18]	4.031s	passed
seqPermTransAlt0	data()[190]	3.874s	passed
seqPermTransAlt1	data()[191]	3.861s	passed
seqPermTransAlt2	data()[192]	3.847s	passed
seqPermTransAlt3	data()[193]	3.814s	passed
seqPermForall	data()[194]	3.950s	passed
seqPermExists	data()[195]	3.929s	passed
schiffl_lemma_2	data()[196]	26.835s	passed
schiffl_thm_1	data()[197]	4.762s	passed
eqSameSeq	data()[198]	4.082s	passed
divResZero2	data()[19]	3.997s	passed
eqTermCut	data()[1]	4.752s	passed
divResOne1	data()[20]	3.936s	passed
divResOne2	data()[21]	3.922s	passed
div_cancel1	data()[22]	3.935s	passed
div_cancel2	data()[23]	3.890s	passed
divAddMultDenom	data()[24]	3.939s	passed
divMinus	data()[25]	3.942s	passed
divMinusDenom	data()[26]	4.010s	passed
divLeastDPos	data()[27]	3.979s	passed
divLeastDNeg	data()[28]	3.907s	passed
divGreatestDPos	data()[29]	3.889s	passed
equivAllRight	data()[2]	4.284s	passed
divGreatestDNeg	data()[30]	3.848s	passed
divIncreasingPos	data()[31]	3.886s	passed
divIncreasingNeg	data()[32]	3.937s	passed
jdiv_zero	data()[33]	3.961s	passed
jdivPulloutMinusNum	data()[34]	4.006s	passed
jdivPulloutMinusDenom	data()[35]	3.962s	passed
jdiv_uniquePosPos	data()[36]	3.952s	passed
jdiv_uniquePosNeg	data()[37]	4.051s	passed
jdiv_uniqueNegPos	data()[38]	4.012s	passed
jdiv_uniqueNegNeg	data()[39]	4.002s	passed
irrflConcrete1	data()[3]	4.296s	passed
jdivMultDenom1	data()[40]	4.052s	passed
jdivMultDenom2	data()[41]	3.984s	passed
mod_geZero	data()[42]	3.905s	passed
mod_lessDenom	data()[43]	3.921s	passed
jmod_NumPos	data()[44]	4.016s	passed
jmod_NumNeg	data()[45]	3.889s	passed
jmod_geZero	data()[46]	3.879s	passed
jmodNumZero	data()[47]	3.864s	passed
jmod_pulloutminusNum	data()[48]	3.889s	passed
jmod_pulloutminusDenom	data()[49]	3.890s	passed
irrflConcrete2	data()[4]	4.147s	passed
jmodUnique1	data()[50]	4.022s	passed
jmodUnique2	data()[51]	3.989s	passed
intDivRem	data()[52]	3.914s	passed
jmodjmod	data()[53]	3.938s	passed
jmodDivisible	data()[54]	3.926s	passed
jmodDivisibleRep	data()[55]	3.832s	passed
jdivAddMultDenom	data()[56]	4.087s	passed
jmodAltZero	data()[57]	3.909s	passed
jmodAddMultDenomZero	data()[58]	3.807s	passed
polyDiv_zero	data()[59]	3.825s	passed
cancel_gtPos	data()[5]	4.071s	passed
polyMod_ltdivDenom	data()[60]	3.879s	passed
bsum_empty	data()[61]	3.866s	passed
bsum_induction_upper	data()[62]	3.886s	passed
bsum_induction_lower	data()[63]	3.949s	passed
bsum_num_of_bounds	data()[64]	4.005s	passed
bsum_num_of_bounds2	data()[65]	3.916s	passed
bsum_induction_upper2	data()[66]	3.983s	passed
bsum_induction_upper_concrete	data()[67]	3.860s	passed
bsum_induction_upper_concrete_2	data()[68]	3.822s	passed
bsum_induction_upper2_concrete	data()[69]	3.854s	passed
cancel_gtNeg	data()[6]	4.048s	passed
bsum_induction_lower_concrete	data()[70]	3.802s	passed
bsum_induction_lower2	data()[71]	3.837s	passed
bsum_induction_lower2_concrete	data()[72]	3.816s	passed
bsum_positive	data()[73]	3.944s	passed
bsum_upper_bound	data()[74]	3.928s	passed
bsum_lower_bound	data()[75]	3.865s	passed
bsum_positive_lower_bound_element	data()[76]	3.994s	passed
bsum_sub_same_index	data()[77]	3.954s	passed
bsum_less_same_index	data()[78]	3.897s	passed
bsum_equal_except_one_index	data()[79]	3.889s	passed
moduloIntIsInInt	data()[7]	4.190s	passed
bsum_num_of_is_max	data()[80]	3.948s	passed
bsum_num_of_is_max2	data()[81]	4.084s	passed
bsum_num_of_is_max3	data()[82]	4.097s	passed
bsum_num_of_is_max4	data()[83]	3.888s	passed
bsum_num_of_lt_max	data()[84]	3.848s	passed
bsum_num_of_lt_max2	data()[85]	3.940s	passed
bsum_num_of_lt_max3	data()[86]	3.859s	passed
bsum_num_of_lt_max4	data()[87]	3.900s	passed
bsum_num_of_gt0	data()[88]	4.033s	passed
bsum_num_of_gt0_alt	data()[89]	3.977s	passed
moduloLongIsInLong	data()[8]	3.954s	passed
bsum_add_concrete	data()[90]	3.829s	passed
bprod_all_positive	data()[91]	3.879s	passed
bprod_split	data()[92]	4.008s	passed
powConcrete0	data()[93]	3.879s	passed
powConcrete1	data()[94]	3.807s	passed
powSplitFactor	data()[95]	3.841s	passed
powAdd	data()[96]	3.846s	passed
powMono	data()[97]	4.124s	passed
powMonoConcrete	data()[98]	3.879s	passed
powMonoConcreteRight	data()[99]	3.913s	passed
moduloShortIsInShort	data()[9]	3.883s	passed
Standard output

578        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
609        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.75ms 
884        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
901        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)

1932       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1935       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1940       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1940       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3679       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10050      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.17s 
10165      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10205      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.7ns 
10220      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10220      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 694.81ns 
10226      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13782      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
13786      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14934      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14962      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.23ms 
14977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485.31ns 
14979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18171      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
18172      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
19242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19258      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.82ms 
19261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19261      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.2ns 
19263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22453      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
22453      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
23533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
23555      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.72ms 
23558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23558      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.5ns 
23559      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26675      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
26675      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
27695      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
27701      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
27706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
27707      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 552.21ns 
27708      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30707      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
30708      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
31727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
31774      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.3ms 
31779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
31779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445ns 
31781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34784      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
34785      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
35800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
35824      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.91ms 
35828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
35828      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 496.21ns 
35829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
39018      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
40010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
40014      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 955.91ns 
40017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
40018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422ns 
40019      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42966      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
42966      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
43966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
43970      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 705.31ns 
43973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
43974      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 452.11ns 
43975      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46878      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
46879      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
47850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
47853      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.41ns 
47856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
47857      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.5ns 
47858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50974      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
50975      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
51988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
51992      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702.01ns 
51995      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
51995      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.31ns 
51996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54932      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
54933      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
55896      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
55899      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 713.11ns 
55902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
55902      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.7ns 
55904      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.92s 
58825      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
59823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
59871      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.5ms 
59881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
59881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 768.81ns 
59883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62871      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
62872      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
63836      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
63876      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.65ms 
63880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
63880      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 460.91ns 
63882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66876      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
66876      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
67827      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
68064      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 227.95ms 
68067      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
68067      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns 
68069      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71061      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
71062      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
72030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
72037      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
72041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
72041      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.31ns 
72042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74934      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
74935      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
75911      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
75915      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
75918      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
75919      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.81ns 
75920      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78808      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
78809      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
79765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
79807      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.95ms 
79812      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
79812      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.2ns 
79813      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82799      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
82800      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
83821      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
83840      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.64ms 
83847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
83847      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 492.01ns 
83849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86857      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
86858      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
87823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
87840      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.35ms 
87843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
87844      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 456ns 
87845      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
90771      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
91753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
91777      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.56ms 
91779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
91779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.2ns 
91780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94693      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
94693      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
95679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
95699      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.93ms 
95702      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
95702      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.4ns 
95703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98679      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
98679      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
99605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
99634      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.87ms 
99635      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
99636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.8ns 
99637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
102557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
103521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
103524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
103525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
103525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.8ns 
103527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
106428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
107404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
107455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.78ms 
107466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
107466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.31ns 
107468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
110366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
111343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
111405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.4ms 
111408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
111408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.8ns 
111409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
114433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
115367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
115416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.73ms 
115417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
115418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.2ns 
115418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
118426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
119387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
119395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.99ms 
119397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
119397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.7ns 
119398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
122306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
123288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
123302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.62ms 
123304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
123304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.1ns 
123305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
126209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
127172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
127190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.97ms 
127193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
127194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.5ns 
127195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
130073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
131030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
131040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
131041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
131041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.4ns 
131042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
133955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
134906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
134924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.81ms 
134928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
134929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.4ns 
134930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
137894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
138855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
138863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ms 
138865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
138865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.5ns 
138866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
141854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
142817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
142825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
142829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
142829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.31ns 
142830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
145855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
146820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
146832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
146834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
146834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.6ns 
146835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
149794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
150729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
150793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.32ms 
150797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
150797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.81ns 
150798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
153731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
154718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
154746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.59ms 
154749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
154749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.81ms 
154751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
157755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
158774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
158796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.97ms 
158799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
158799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.81ns 
158801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
161820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
162789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
162809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.19ms 
162811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
162811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.7ns 
162812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
165777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
166791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
166811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.16ms 
166813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
166813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
166814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
169844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
170812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
170863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.97ms 
170865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
170865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.61ns 
170869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
173887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
174844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
174847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
174849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
174849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.6ns 
174850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
177724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
178744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
178748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
178756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
178757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 481.31ns 
178758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
181738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
182665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
182674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.59ms 
182675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
182676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
182676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
185673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
186681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
186690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.93ms 
186693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
186693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344ns 
186694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
189604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
190558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
190579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.21ms 
190581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
190581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.3ns 
190582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
193469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
194447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
194457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.81ms 
194460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
194460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344ns 
194461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
197382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
198318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
198322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
198324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
198325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357ns 
198326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
201247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
202207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
202211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
202213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
202213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
202214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
205113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
206086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
206101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ms 
206103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
206103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.4ns 
206104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
209024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
210021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
210123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.1ms 
210126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
210126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347ns 
210128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
213074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
214006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
214111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 96.64ms 
214114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
214115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.31ns 
214116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
217043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
218021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
218026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
218027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
218028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.11ns 
218029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
220916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
221918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
221964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.74ms 
221966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
221966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.3ns 
221967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
224896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
225853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
225890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.38ms 
225891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
225892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 434.11ns 
225893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
228792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
229719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
229722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
229724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
229724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.1ns 
229726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
232622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
233574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
233808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.1ms 
233812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
233812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 758.11ns 
233818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
236735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
237704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
237717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.86ms 
237720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
237720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.8ns 
237721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
240566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
241516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
241525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.46ms 
241527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
241527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
241528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
244405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
245330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
245350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.95ms 
245352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
245352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
245353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
248261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
249213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
249228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
249231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
249231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
249231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
252101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
253091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
253095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
253096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
253096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
253097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
256029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
256976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
256982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
256983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
256983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
256984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
259950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
260903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
260930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.17ms 
260932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
260932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
260933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
263907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
264915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
264935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.69ms 
264937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
264937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
264938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
267878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
268833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
268851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.61ms 
268853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
268853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
268854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
271804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
272830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
272834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
272837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
272837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.8ns 
272838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
275744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
276689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
276695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
276697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
276697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.2ns 
276698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
279584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
280510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
280517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 
280519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
280519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.9ns 
280521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
283420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
284368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
284372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
284373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
284373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
284374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
287223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
288170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
288173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 928.01ns 
288174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
288175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
288175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
291034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
292006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
292010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
292012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
292012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.6ns 
292013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
294901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
295823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
295826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
295828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
295828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
295829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
298741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
299698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
299769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.06ms 
299772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
299772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.7ns 
299774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
302704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
303655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
303698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.63ms 
303700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
303700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
303701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
306563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
307527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
307563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.7ms 
307565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
307565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
307566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
310580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
311502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
311557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.71ms 
311558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
311559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
311559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
314512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
315474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
315511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.42ms 
315513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
315513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
315514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
318358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
319337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
319407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.98ms 
319410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
319410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
319411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
322311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
323264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
323297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.66ms 
323299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
323299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
323300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
326296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
327220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
327245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.44ms 
327246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
327247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
327247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
330252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
331294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
331329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.73ms 
331331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
331331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
331332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
334404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
335399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
335426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.47ms 
335427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
335427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
335428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
338330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
339281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
339314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.3ms 
339316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
339316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
339317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
342212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
343132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
343162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.17ms 
343164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
343164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns 
343165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
346072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
347072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
347102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.88ms 
347104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
347104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
347105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
349979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
350931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
350961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.07ms 
350963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
350963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
350964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
353888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
354835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
354861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.8ms 
354862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
354863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
354863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
357858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
358863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
358894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.26ms 
358896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
358896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
358896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
361889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
362840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
362871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.62ms 
362874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
362874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.8ns 
362875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
365742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
366691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
366700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.17ms 
366702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
366702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
366703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
369620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
370558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
370580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.45ms 
370581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
370581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
370582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
373609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
374582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
374587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
374588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
374588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
374589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
377516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
378464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
378466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 670.91ns 
378468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
378468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
378468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
381319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
382271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
382274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 897.51ns 
382275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
382275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
382276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
385157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
386106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
386114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.81ms 
386116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
386116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
386116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
389012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
389950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
389960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.65ms 
389961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
389961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
389962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
393096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
394070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
394085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms 
394086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
394086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
394087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
396962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
397959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
397963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
397964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
397964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
397965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
400860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
401873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
401876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 674.31ns 
401878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
401878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.9ns 
401879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
404776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
405802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
405808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 
405810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
405810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.5ns 
405811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
408685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
409608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
409611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 710.11ns 
409612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
409612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
409613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
412501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
413439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
413441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 656.01ns 
413442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
413443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
413443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
416275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
417220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
417223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 688.61ns 
417224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
417224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
417225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
420135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
421127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
421132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
421133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
421133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
421134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
424154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
425074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
425085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
425087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
425087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
425088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
427975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
428928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
428933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
428934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
428934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
428935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
431796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
432739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
432747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
432749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
432749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
432749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
435621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
436564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
436569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
436570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
436571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
436571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
439420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
440351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
440370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.28ms 
440372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
440372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
440373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
443335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
444314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
444318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
444320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
444320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
444320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
447187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
448136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
448140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
448141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
448141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
448142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
451008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
451987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
451992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
451994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
451994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
451995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
455023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
455942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
455962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.56ms 
455963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
455963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
455964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
458857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
459806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
459811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 648.81ns 
459814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
459814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
459815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
462683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
463619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
463664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.86ms 
463665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
463666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
463666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
466515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
467464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
467468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
467469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
467470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
467470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
470356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
471278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
471304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.45ms 
471305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
471305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
471306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
474226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
475171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
475195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.28ms 
475197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
475197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
475197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
478067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
479020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
479047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.53ms 
479049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
479049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
479050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
481956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
482881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
482884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.61ns 
482886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
482886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.1ns 
482887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
485814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
486766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
486773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.46ms 
486774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
486774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
486775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
489633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
490576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
490579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
490581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
490581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
490581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
493472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
494425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
494428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 848.21ns 
494429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
494429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
494430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
497307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
498249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
498252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 908.91ns 
498253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
498253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
498254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
501166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
502180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
502184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
502185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
502185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
502186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
505120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
506059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
506062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
506069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
506070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.16ms 
506072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
509061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
510063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
510075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.21ms 
510077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
510077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
510078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
513094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
514047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
514060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.62ms 
514062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
514062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
514063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
516964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
517921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
517934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.82ms 
517936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
517936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.2ns 
517937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
520872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
521842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
521857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.46ms 
521858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
521858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
521859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
524755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
525705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
525712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
525714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
525714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.5ns 
525716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
528637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
529607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
529614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
529615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
529615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
529616     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.99s 
532601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
533599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
533601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 746.71ns 
533603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
533603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
533603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
536489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
537450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
537453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
537455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
537455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
537456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
540326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
541257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
541259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931.51ns 
541261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
541261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
541262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
544190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
545189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
545201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.42ms 
545203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
545203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
545204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
548150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
549108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
549115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ms 
549117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
549117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
549118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
552184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
553136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
553143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ms 
553145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
553145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
553146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
556039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
556974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
556976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 787.11ns 
556978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
556978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
556979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
559880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
560907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
560910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703.71ns 
560911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
560911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
560912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
563853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
564786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
564791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
564792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
564792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
564793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
567681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
568637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
568641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
568642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
568642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
568643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
571608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
572540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
572578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.86ms 
572579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
572579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
572581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
575437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
576400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
576403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
576405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
576405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
576406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
579338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
580295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
580301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
580302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
580302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
580303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
583173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
584124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
584128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
584130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
584130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
584130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
587015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
587965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
587977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ms 
587978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
587979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
587979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
590842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
591774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
591776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 772.11ns 
591777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
591777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
591778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
594646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
595640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
595648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.09ms 
595649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
595649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
595650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
598529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
599486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
599488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
599490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
599490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
599490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
602361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
603290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
603293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 987.21ns 
603294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
603294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
603295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
606184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
607200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
607205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
607211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
607211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.5ns 
607212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
610183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
611182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
611186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
611189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
611189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.8ns 
611190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
614061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
614982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
614986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
614988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
614988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
614988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
617890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
618848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
618853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
618856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
618856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
618857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
621781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
622774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
622782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.04ms 
622783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
622783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
622784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
625739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
626700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
626717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.8ms 
626718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
626718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
626719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
629639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
630601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
630620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.48ms 
630621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
630621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
630622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
633536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
634495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
634507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.09ms 
634509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
634509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.2ns 
634510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
637382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
638343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
638356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.79ms 
638357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
638358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
638358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
641373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
642332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
642362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.97ms 
642363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
642363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
642364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
645224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
646174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
646204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.58ms 
646206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
646206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
646207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
649210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
650189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
650218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.04ms 
650219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
650219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
650220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
653174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
654132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
654150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.78ms 
654152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
654152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
654153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
657052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
658009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
658045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.52ms 
658046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
658046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
658047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
660942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
661906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
661963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.56ms 
661965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
661965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
661966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
664827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
665783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
665829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.87ms 
665830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
665830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
665831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
668825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
669782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
669874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.76ms 
669875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
669876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
669876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
672860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
673798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
673851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.89ms 
673853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
673853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
673854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
676794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
677828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
677987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 152.13ms 
677990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
677990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
677991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
680937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
681929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
681938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
681940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
681940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
681940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
684883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
685846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
685855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
685856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
685856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
685857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
688810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
689773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
689779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
689781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
689781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
689781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
692672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
693631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
693652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.16ms 
693654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
693654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
693655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
696544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
697504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
697517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.73ms 
697518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
697518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
697519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
700452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
701459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
701463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
701465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
701465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
701466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
704447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
705393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
705412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17ms 
705413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
705413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
705414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
708316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
709308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
709329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.11ms 
709330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
709330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
709331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
712228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
713207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
713229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.91ms 
713230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
713230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
713231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
716299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
717326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
717330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
717332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
717332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
717332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
720241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
721213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
721217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
721219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
721219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
721220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
724110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
725063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
725070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
725071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
725071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
725072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
727961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
728919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
728925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
728927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
728927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
728928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
731789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
732830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
732910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.36ms 
732911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
732911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
732912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
735784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
736737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
736768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.36ms 
736769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
736769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
736770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
739668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
740628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
740654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.66ms 
740656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
740656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
740657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
743533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
744505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
744508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 339.4ns 
744510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
744510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219ns 
744512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
747401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
748363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
748627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 252.86ms 
748630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
748631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.6ns 
748632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
751579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
751579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
752593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
752654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.49ms 
752656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
752656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.6ns 
752657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
755525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
755525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
756526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
756529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 433.21ns 
756530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
756530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.1ns 
756531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
759426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
760387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
760389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 430.21ns 
760391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
760391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
760392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
763272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
764234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
764236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 422.51ns 
764238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
764238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
764238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
767100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
768048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
768051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 546.81ns 
768052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
768052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
768053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
770920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
771873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
771981     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
772000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 125.08ms 
772002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
772002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
772003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
774904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
775875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
775928     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
775929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.69ms 
775931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
775931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
775933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
778980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
779947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
779949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 
779981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
780037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
780066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
780076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
780086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
780089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
780091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
780095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
780101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
780103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
780110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
780111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
780361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
780362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
780363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
780364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
780365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
780485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
780487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
780488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
780490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
780491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
780492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
780675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
780677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
780678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
780678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
780679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
780681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
780826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
780828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
780829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
780829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
780830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
780831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
780839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
780840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
780841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
780843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
780844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
780845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
780853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
780853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
780854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
780855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
780856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
780857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
781011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
781012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
781013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
781155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
781157     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)'' 
781160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
781161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
781162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
781163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
781164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
781164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
781169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
781170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
781171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
781172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
781173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
781303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
781307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
781309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
781310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
781311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
781311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
781312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
781468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
781470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
781471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
781473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
781473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
781474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
781474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
781476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
781592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
781594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
781727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
781733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
781739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
781740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
781741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
781742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
781743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
781743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
781744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
781745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
781756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
781762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
781905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
781906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
781907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
781908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
781909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
781910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
781910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
781911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
781986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
781994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
782133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
782134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
782136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
782138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
782139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
782140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
782313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
782318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
782319     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)'' 
782321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
782322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
782323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
782324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
782324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
782338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
782339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
782340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
782341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
782500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
782502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
782504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
782505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
782512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
782513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
782693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
782695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
782697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
782700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
782700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
782701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
782702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
782704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
782824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
782826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
782921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
782922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
782923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
782928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
782932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
782937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
783087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
783089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
783090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
783092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
783104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
783206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
787584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
787585     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)'' 
787591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
787592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
787593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
787593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
787594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
787602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
787604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
787605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
787606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
787607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
787767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
787771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
787772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
787773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
787774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
787774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
787775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
787886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
787887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
787888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
787890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
787890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
787891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
787891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
787892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
787982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
787984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
788077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
788082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
788087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
788088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
788088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
788089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
788101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
788199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
788200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
788201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
788202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
788286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
788296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
788297     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)'' 
788299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
788300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
788301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
788301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
788302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
788314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
788315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
788316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
788317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
788318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
788419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
788420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
788421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
788422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
788423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
788529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
788534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
788535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
788535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
788536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
788537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
788537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
788649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
788650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
788651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
788653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
788653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
788654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
788654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
788655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
788656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
788657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
788658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
788659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
788659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
788660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
788661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
788772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
788773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
788780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
788875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
788974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
788976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
788977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
788977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
788978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
788979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
788979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
788980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
788981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
789096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
789105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
789219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
789220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
789221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
789222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
789223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
789223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
789223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
789224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
789230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
789231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
789324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
789330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
789336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
789451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
789453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
789454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
789455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
789455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
789456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
789456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
789457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
789521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
789522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
789523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
789523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
789524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
789531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
789537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
789722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
789823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
789824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
789825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
789826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
790018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
790118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
790119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
793737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
793743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
793744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
793745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
793746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
793878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
793879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
793881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
793881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
793882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
794004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
797486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
801260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
801265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
801266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
801267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
801268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
801401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
801403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
801404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
801405     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)' ...' 
801407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
802766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
802766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
802767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
805794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
806786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
806787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
806788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
806797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
806810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
806813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
806815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
806816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
806821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
806823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
806827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
806830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
806830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
806841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
806843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
806844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
806899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
806901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
806901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
806902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
806903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
806978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
806978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
806980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
806981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
806982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
806986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
806987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
806988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
806989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
806990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
806991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
807085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
807086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
807087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
807088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
807089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
807090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
807183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
807184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
807185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
807186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
807187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
807188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
807188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
807189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
807190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
807191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
807191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
807192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
807193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
807193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
807194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
807195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
807195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
807196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
807198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
807200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
807240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
807241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
807294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
807295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
807297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
807299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
807300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
807300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
807346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
807349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
807350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
807352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
807354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
807355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
807355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
807403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
807406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
807409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
807467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
807528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
807529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.7ns 
807530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
810540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
810541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
811563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
811604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.55ms