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

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

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

303        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
327        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.62ms 
556        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572        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)

1562       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1564       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1565       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1565       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2761       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7463       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.91s 
7522       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7551       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.8ns 
7563       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7564       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 479.72ns 
7567       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
10241      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11189      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.26ms 
11211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11211      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.41ns 
11216      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13765      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
13765      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
14548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
14562      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.55ms 
14564      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
14564      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.8ns 
14566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16979      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
16980      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
17771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
17777      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
17780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
17781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.91ns 
17782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20222      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
20223      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21005      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21010      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
21012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21012      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.21ns 
21013      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23292      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
23292      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24075      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24116      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.5ms 
24120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.91ns 
24122      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26399      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
26399      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27203      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.83ms 
27205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27206      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.21ns 
27207      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29459      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
29459      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
30206      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
30210      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 661.52ns 
30212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
30213      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.31ns 
30214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32472      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
32472      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
33219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
33225      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
33228      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
33229      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 799.73ns 
33230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35501      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
35502      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
36240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
36243      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.32ns 
36245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
36245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.11ns 
36246      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38473      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
38473      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
39228      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
39230      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.72ns 
39233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
39233      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.11ns 
39236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41476      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
41477      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
42214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
42217      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.42ns 
42219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
42220      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.71ns 
42221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44461      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
44462      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
45173      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
45216      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.64ms 
45221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
45221      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.31ns 
45223      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47462      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
47463      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
48193      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
48230      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.32ms 
48232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
48232      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
48233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50459      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
50460      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
51190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
51401      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 201.2ms 
51404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
51404      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.81ns 
51405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53646      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
53647      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
54374      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
54379      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
54381      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
54381      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
54382      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56615      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
56615      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
57322      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
57325      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
57329      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
57329      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.01ns 
57330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59562      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
59563      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
60288      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
60326      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.12ms 
60329      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
60329      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.91ns 
60330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62540      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
62540      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
63273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
63288      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.89ms 
63290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
63290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.51ns 
63291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
65498      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
66222      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
66236      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.72ms 
66237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
66237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
66238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68469      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
68469      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
69174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
69189      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ms 
69190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
69191      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
69191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71426      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
71427      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
72152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
72166      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.45ms 
72168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
72168      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
72169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74371      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
74371      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
75096      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
75119      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.57ms 
75120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
75120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.8ns 
75121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77320      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
77320      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
78053      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
78055      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 914.23ns 
78056      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
78056      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
78057      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80275      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
80275      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
80999      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
81037      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.05ms 
81048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
81048      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
81049      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83283      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
83283      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
84022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
84091      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.24ms 
84097      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
84099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.6ns 
84100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
86335      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
87110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
87151      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.42ms 
87152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
87153      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.11ns 
87153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89352      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
89352      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
90092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
90100      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms 
90103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
90103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.01ns 
90104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92324      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
92324      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
93027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
93039      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.45ms 
93040      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
93040      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.1ns 
93041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
95254      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
95974      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
95985      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.04ms 
95986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
95986      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
95987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98182      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
98183      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
98905      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
98912      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
98914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
98915      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.21ns 
98916      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
101113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
101836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
101843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
101844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
101844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
101845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
104057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
104760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
104766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
104767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
104767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
104768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
107007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
107713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
107716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
107721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
107721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.71ns 
107722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
109937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
110679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
110689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ms 
110691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
110691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.41ns 
110692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
112886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
113608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
113666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.67ms 
113668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
113668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.61ns 
113669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
115861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
116581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
116598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.92ms 
116600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
116600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.91ns 
116601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
118807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
119507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
119524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.02ms 
119525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
119525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
119526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
121734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
122455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
122472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.04ms 
122474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
122474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
122474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
124667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
125389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
125405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.4ms 
125407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
125407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
125408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
127597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
128325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
128366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.72ms 
128368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
128369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.81ns 
128370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
130579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
131279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
131281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 880.03ns 
131283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
131283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
131283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
133503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
134223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
134227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
134228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
134228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
134229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
136417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
137138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
137148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.77ms 
137153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
137153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.11ns 
137155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
139344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
140066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
140074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
140076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
140076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.41ns 
140077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
142281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
142980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
142998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
142999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
142999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
143000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
145204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
145923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
145931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.47ms 
145932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
145932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
145933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
148118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
148847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
148851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
148854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
148855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.81ns 
148856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
151068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
151788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
151791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
151792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
151792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
151793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
153994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
154693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
154697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
154698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
154698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
154699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
156904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
157622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
157689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.44ms 
157690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
157691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.21ns 
157692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
159885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
160607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
160689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.64ms 
160691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
160692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.01ns 
160693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
162879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
163596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
163599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
163600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
163600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
163601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
165803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
166503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
166536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.96ms 
166538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
166539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.42ns 
166539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
168740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
169455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
169483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.62ms 
169484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
169484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
169485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
171680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
172399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
172401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
172402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
172402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
172403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
174602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
175333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
175471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 123.81ms 
175472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
175473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85ns 
175473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
177688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
178385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
178396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.83ms 
178397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
178397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
178398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
180597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
181313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
181321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.71ms 
181322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
181322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
181323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
183520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
184236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
184266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.89ms 
184268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
184268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.81ns 
184269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
186455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
187171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
187183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.78ms 
187184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
187184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
187185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
189385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
190080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
190084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
190085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
190085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
190086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
192283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
192998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
193002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
193003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
193003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
193004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
195188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
195904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
195926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.83ms 
195928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
195928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
195928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
198113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
198835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
198855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.33ms 
198856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
198856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
198857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
201063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
201787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
201802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.34ms 
201803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
201803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
201804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
204008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
204727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
204730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
204732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
204732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
204733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
206925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
207642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
207647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
207648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
207648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.31ns 
207649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
209829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
210544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
210549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
210550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
210550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
210551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
212750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
213445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
213448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
213449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
213450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
213450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
215647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
216361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
216363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.92ns 
216364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
216364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
216365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
218546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
219261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
219265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
219266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
219266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
219266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
221447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
222162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
222164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
222165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
222165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
222166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
224345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
225061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
225110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.06ms 
225112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
225112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.51ns 
225113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
227326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
228020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
228079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.99ms 
228080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
228080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
228081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
230266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
230982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
231013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.59ms 
231016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
231016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
231017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
233199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
233913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
233956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.8ms 
233957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
233957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
233958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
236160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
236854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
236884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.28ms 
236885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
236885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
236886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
239086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
239809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
239863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.06ms 
239865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
239865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
239866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
242050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
242766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
242795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.62ms 
242797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
242797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.21ns 
242798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
244982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
245696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
245716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.1ms 
245717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
245717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
245718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
247918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
248619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
248650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.16ms 
248652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
248652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
248653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
250860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
251574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
251593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.78ms 
251595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
251595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
251595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
253777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
254506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
254535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.34ms 
254537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
254537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.71ns 
254538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
256828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
257556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
257582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.94ms 
257583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
257583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
257584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
259786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
260482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
260507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.77ms 
260508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
260508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
260509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
262712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
263427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
263452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.03ms 
263454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
263454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
263454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
265638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
266352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
266373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.18ms 
266374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
266374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
266375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
268555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
269275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
269315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.74ms 
269316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
269316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
269317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
271516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
272211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
272235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.5ms 
272236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
272236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
272237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
274441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
275155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
275162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 
275163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
275163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
275164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
277349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
278064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
278081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.47ms 
278082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
278082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
278083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
280261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
280976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
280980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
280981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
280981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
280981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
283180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
283875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
283877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 574.22ns 
283878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
283878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
283879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
286080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
286805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
286808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 735.13ns 
286809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
286810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.61ns 
286810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
288990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
289704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
289712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
289713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
289713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
289713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
291893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
292615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
292621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
292622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
292622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
292623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
294796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
295513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
295525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ms 
295526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
295527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
295527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
297724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
298420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
298424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
298425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
298425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
298425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
300623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
301339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
301341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 490.72ns 
301342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
301342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
301343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
303526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
304244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
304250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
304251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
304251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
304251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
306430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
307147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
307149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.72ns 
307150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
307150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
307151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
309346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
310041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
310043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 544.22ns 
310044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
310044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
310045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
312241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
312956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
312958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 564.82ns 
312959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
312959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
312959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
315138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
315855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
315858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
315859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
315859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
315860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
318040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
318756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
318764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.57ms 
318765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
318765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
318766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
320967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
321663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
321667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
321668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
321668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
321668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
323862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
324577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
324583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.78ms 
324584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
324584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
324585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
326765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
327485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
327489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
327490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
327490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
327491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
329666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
330386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
330404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.01ms 
330406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
330406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.11ns 
330407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
332609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
333306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
333309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
333310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
333310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
333310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
335506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
336222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
336228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
336230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
336231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.01ns 
336231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
338413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
339129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
339132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
339133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
339133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
339134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
341314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
342030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
342046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
342047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
342047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
342048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
344250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
344946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
344950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 493.22ns 
344952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
344952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
344953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
347144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
347855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
347892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.42ms 
347893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
347893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
347893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
350075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
350790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
350793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
350794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
350794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
350795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
352968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
353682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
353703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.69ms 
353704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
353704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
353704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
355901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
356597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
356621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.15ms 
356622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
356622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
356623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
358836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
359552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
359575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.05ms 
359576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
359576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
359577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
361790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
362512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
362514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 524.62ns 
362517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
362517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
362517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
364719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
365417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
365422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
365423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
365423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.5ns 
365424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
367623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
368341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
368344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
368345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
368345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
368345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
370525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
371243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
371245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 711.13ns 
371246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
371246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
371247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
373446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
374145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
374147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
374151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
374151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.11ns 
374152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
376351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
377075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
377078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
377079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
377079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
377079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
379258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
379977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
379980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
379981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
379981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
379981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
382174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
382875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
382884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.75ms 
382885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
382885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
382886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
385081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
385802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
385814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.21ms 
385815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
385815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
385816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
387996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
388719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
388732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.54ms 
388734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
388734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.61ns 
388735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
390929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
391653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
391666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.35ms 
391667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
391668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.51ns 
391668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
393852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
394579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
394584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
394585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
394585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
394586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
396781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
397507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
397513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 
397514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
397514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
397514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
399694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
400421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
400423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.33ns 
400424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
400424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
400425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
402619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
403324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
403327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
403328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
403328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
403329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
405523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
406247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
406249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 899.03ns 
406250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
406250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
406250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
408448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
409154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
409164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.29ms 
409165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
409165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
409166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
411359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
412082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
412086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
412087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
412087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
412088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
414264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
414989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
414996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.42ms 
414998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
414998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.51ns 
414999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
417193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
417916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
417918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 640.22ns 
417919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
417919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
417920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
420094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
420823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
420825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.32ns 
420826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
420826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
420827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
423018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
423741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
423745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
423746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
423746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
423747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
425939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
426646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
426648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
426649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
426649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
426650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
428847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
429572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
429575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
429576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
429576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.4ns 
429576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
431768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
432473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
432476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
432477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
432477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
432478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
434669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
435392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
435397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 
435398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
435398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
435399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
437592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
438316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
438318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
438319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
438319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
438320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
440500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
441225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
441236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.16ms 
441237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
441237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
441237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
443434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
444158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
444160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.82ns 
444161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
444161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
444162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
446357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
447064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
447071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
447072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
447072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
447073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
449272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
449996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
449998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 817.03ns 
449999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
449999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
450000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
452192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
452914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
452916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 792.03ns 
452917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
452917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
452918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
455092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
455814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
455819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
455820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
455820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
455821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
458009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
458732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
458735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
458736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
458736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
458737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
460925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
461648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
461651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
461652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
461652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
461653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
463833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
464557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
464561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
464563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
464563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
464564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
466758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
467482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
467487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms 
467488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
467488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
467489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
469686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
470411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
470425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.05ms 
470426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
470426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.5ns 
470426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
472625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
473330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
473345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.35ms 
473346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
473346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
473347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
475539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
476263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
476273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.35ms 
476274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
476274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
476275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
478467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
479190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
479200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.68ms 
479201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
479201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
479202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
481395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
482118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
482143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.32ms 
482145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
482145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
482145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
484349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
485054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
485103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.22ms 
485104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
485104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
485105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
487283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
488005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
488029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.41ms 
488030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
488030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
488031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
490225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
490951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
490965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
490966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
490966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
490967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
493183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
493926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
493974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.99ms 
493975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
493975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
493976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
496170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
496893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
496940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.91ms 
496941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
496941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
496942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
499136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
499862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
499899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.1ms 
499900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
499900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
499901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
502096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
502819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
502861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.11ms 
502862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
502862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
502862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
505060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
505765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
505809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.36ms 
505810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
505810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
505811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
508008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
508736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
508853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 110.37ms 
508855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
508855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
508855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
511057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
511783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
511791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.85ms 
511792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
511792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
511793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
513988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
514711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
514719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 
514720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
514720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
514720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
516907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
517632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
517637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.55ms 
517638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
517639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
517639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
519829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
520551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
520568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.38ms 
520570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
520570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
520570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
522759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
523483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
523493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.67ms 
523494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
523494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
523495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
525689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
526414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
526417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
526418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
526418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
526418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
528609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
529332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
529349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.21ms 
529350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
529350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
529350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
531543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
532266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
532282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.99ms 
532283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
532283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
532284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
534481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
535204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
535223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
535224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
535224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
535224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
537418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
538141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
538144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
538147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
538147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.71ns 
538148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
540340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
541065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
541069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
541070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
541070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
541071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
543262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
543986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
543992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
543993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
543993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
543994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
546193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
546936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
546942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.63ms 
546943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
546943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
546944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
549150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
549876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
549944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.47ms 
549946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
549946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
549947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
552153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
552882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
552912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.12ms 
552913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
552913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
552914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
555108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
555832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
555853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.5ms 
555854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
555854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
555855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
558063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
558790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
558792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 244.51ns 
558794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
558794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
558795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
560991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
561717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
561923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.09ms 
561925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
561925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.11ns 
561926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
564128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
564857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
564906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.48ms 
564907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
564907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
564908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
567100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
567825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
567827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 359.61ns 
567829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
567829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.31ns 
567829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
570019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
570744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
570745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 333.31ns 
570746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
570747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
570747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
572957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
573683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
573685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 312.81ns 
573686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
573686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
573686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
575880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
576605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
576606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 417.32ns 
576608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
576608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
576608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
578796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
579520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
579605     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
579618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 95.57ms 
579620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
579620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.71ns 
579621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
581823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
582550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
582601     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
582602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.37ms 
582603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
582604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
582605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
584819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
585546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
585548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 
585570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
585618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
585661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
585668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
585676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
585679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
585680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
585683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
585688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
585690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
585696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
585697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
585921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
585923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
585924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
585925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
585926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
586051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
586052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
586054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
586056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
586058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
586058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
586233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
586235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
586237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
586238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
586239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
586240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
586356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
586359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
586360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
586361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
586362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
586363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
586370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
586372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
586373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
586375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
586379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
586380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
586388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
586389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
586391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
586391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
586392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
586393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
586519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
586520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
586522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
586626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
586628     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)'' 
586631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
586632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
586633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
586635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
586636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
586638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
586645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
586646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
586648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
586648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
586649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
586750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
586753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
586755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
586756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
586757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
586757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
586759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
586869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
586871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
586872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
586874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
586874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
586875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
586876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
586878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
586960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
586961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
587046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
587050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
587054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
587056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
587058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
587060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
587061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
587061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
587062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
587063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
587070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
587075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
587168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
587169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
587171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
587172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
587173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
587173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
587174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
587175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
587225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
587230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
587318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
587320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
587322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
587324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
587324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
587325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
587436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
587440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
587443     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)'' 
587445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
587446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
587447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
587447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
587448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
587456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
587459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
587463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
587464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
587552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
587554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
587556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
587558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
587558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
587559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
587665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
587666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
587667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
587668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
587669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
587669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
587669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
587670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
587746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
587747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
587815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
587815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
587816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
587820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
587823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
587827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
587939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
587940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
587941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
587941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
587951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
588030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
591597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
591598     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)'' 
591603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
591604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
591604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
591605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
591605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
591612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
591614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
591615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
591615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
591616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
591705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
591709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
591710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
591710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
591711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
591711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
591712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
591804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
591805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
591805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
591806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
591807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
591807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
591808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
591809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
591882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
591883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
591954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
591958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
591961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
591962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
591963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
591964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
591973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
592050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
592051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
592052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
592052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
592123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
592168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
592169     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)'' 
592171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
592171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
592172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
592172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
592173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
592183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
592184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
592185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
592185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
592186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
592270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
592271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
592272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
592273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
592274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
592361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
592365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
592366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
592366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
592367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
592367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
592368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
592463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
592465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
592465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
592467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
592467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
592467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
592468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
592469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
592470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
592470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
592471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
592471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
592472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
592472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
592473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
592557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
592558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
592564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
592639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
592717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
592718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
592719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
592720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
592720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
592721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
592721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
592721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
592722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
592805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
592811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
592901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
592902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
592902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
592904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
592904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
592904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
592905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
592906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
592910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
592911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
592988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
592993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
592998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
593094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
593095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
593096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
593097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
593097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
593097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
593097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
593098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
593150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
593151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
593152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
593152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
593153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
593158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
593165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
593278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
593363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
593364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
593365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
593366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
593527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
593612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
593613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
596580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
596585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
596586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
596586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
596587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
596698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
596699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
596700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
596701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
596701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
596804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
599728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
602856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
602861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
602862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
602863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
602863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
602973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
602975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
602976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
602976     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)' ...' 
602978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
604098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
604098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
604099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
606353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
607100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
607101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ns 
607102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
607112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
607123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
607126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
607128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
607128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
607133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
607134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
607138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
607141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
607141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
607151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
607153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
607154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
607208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
607209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
607209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
607210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
607210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
607286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
607286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
607287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
607288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
607288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
607291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
607292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
607292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
607293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
607294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
607294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
607382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
607382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
607383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
607384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
607385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
607385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
607534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
607535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
607535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
607536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
607536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
607537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
607538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
607538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
607539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
607539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
607540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
607540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
607541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
607541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
607542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
607542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
607543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
607544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
607544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
607546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
607586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
607587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
607651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
607652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
607654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
607655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
607656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
607656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
607714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
607717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
607718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
607719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
607720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
607721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
607722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
607782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
607784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
607787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
607858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
607920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
607920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.61ns 
607921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
610173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
610940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
610970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.31ms