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

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

Test	Method name	Duration	Result
powPositive	data()[100]	3.855s	passed
powPositiveConcrete	data()[101]	4.014s	passed
powGeq1Concrete	data()[102]	4.359s	passed
pow2InIntLower	data()[103]	4.056s	passed
pow2InIntUpper	data()[104]	3.772s	passed
logSelfConcrete	data()[105]	4.025s	passed
log1Concrete	data()[106]	3.934s	passed
logProduct	data()[107]	3.901s	passed
logTimesBaseConcrete	data()[108]	4.024s	passed
logProdIdentity	data()[109]	3.928s	passed
moduloByteIsInByte	data()[10]	4.067s	passed
logProdIdentityConcrete	data()[110]	3.790s	passed
logPowIdentity	data()[111]	3.768s	passed
logPowIdentityConcrete	data()[112]	3.819s	passed
logPositive	data()[113]	3.896s	passed
logPositiveConcrete	data()[114]	3.800s	passed
logMono	data()[115]	3.788s	passed
logMonoConcrete	data()[116]	3.744s	passed
powLogLess	data()[117]	3.829s	passed
powLogMore2	data()[118]	3.957s	passed
logLessThanPow	data()[119]	4.025s	passed
moduloCharIsInChar	data()[11]	4.007s	passed
logLessThanPowConcrete	data()[120]	4.134s	passed
logSqueeze	data()[121]	3.876s	passed
ifthenelse_equals	data()[122]	3.777s	passed
ifthenelse_equals_1	data()[123]	3.769s	passed
ifthenelse_equals_2	data()[124]	3.896s	passed
disjointWithSingleton1	data()[125]	3.846s	passed
disjointWithSingleton2	data()[126]	3.960s	passed
disjointArrayRanges	data()[127]	3.880s	passed
disjointArrayRangeAllFields1	data()[128]	3.770s	passed
disjointArrayRangeAllFields2	data()[129]	3.805s	passed
div_unique1	data()[12]	4.082s	passed
seqSelfDefinition	data()[130]	3.765s	passed
seqOutsideValue	data()[131]	3.858s	passed
castedGetAny	data()[132]	4.021s	passed
seqGetAlphaCast	data()[133]	3.959s	passed
getOfSeqSingleton	data()[134]	3.815s	passed
getOfSeqSingletonConcrete	data()[135]	3.974s	passed
getOfSeqConcat	data()[136]	4.074s	passed
getOfSeqSub	data()[137]	3.937s	passed
getOfSeqReverse	data()[138]	3.771s	passed
lenOfSeqEmpty	data()[139]	3.869s	passed
div_unique2	data()[13]	4.034s	passed
lenOfSeqSingleton	data()[140]	3.934s	passed
lenOfSeqConcat	data()[141]	3.978s	passed
lenOfSeqSub	data()[142]	3.718s	passed
lenOfSeqReverse	data()[143]	3.788s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.864s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.824s	passed
getOfSeqSingletonEQ	data()[146]	3.777s	passed
getOfSeqConcatEQ	data()[147]	3.826s	passed
getOfSeqSubEQ	data()[148]	3.825s	passed
getOfSeqReverseEQ	data()[149]	3.841s	passed
div_exists	data()[14]	4.198s	passed
lenOfSeqEmptyEQ	data()[150]	3.894s	passed
lenOfSeqSingletonEQ	data()[151]	3.792s	passed
lenOfSeqConcatEQ	data()[152]	3.843s	passed
lenOfSeqSubEQ	data()[153]	3.927s	passed
lenOfSeqReverseEQ	data()[154]	3.797s	passed
getOfSeqDefEQ	data()[155]	3.761s	passed
lenOfSeqDefEQ	data()[156]	3.853s	passed
seqConcatWithSeqEmpty1	data()[157]	3.937s	passed
seqConcatWithSeqEmpty2	data()[158]	3.821s	passed
seqReverseOfSeqEmpty	data()[159]	3.937s	passed
div_one	data()[15]	3.873s	passed
subSeqComplete	data()[160]	4.045s	passed
subSeqTailR	data()[161]	3.894s	passed
subSeqTailL	data()[162]	3.841s	passed
subSeqTailEQR	data()[163]	3.905s	passed
subSeqTailEQL	data()[164]	3.831s	passed
seqDef_split	data()[165]	4.031s	passed
seqDef_induction_upper	data()[166]	3.886s	passed
seqDef_induction_upper_concrete	data()[167]	3.972s	passed
seqDef_induction_lower	data()[168]	3.878s	passed
seqDef_induction_lower_concrete	data()[169]	3.938s	passed
jdiv_one	data()[16]	3.958s	passed
seqDef_split_in_three	data()[170]	4.114s	passed
seqDef_empty	data()[171]	3.828s	passed
seqDef_one_summand	data()[172]	3.882s	passed
seqDef_lower_equals_upper	data()[173]	3.854s	passed
seqDefOfSeq	data()[174]	3.844s	passed
seqSelfDefinitionEQ2	data()[175]	3.906s	passed
indexOfSeqSingleton	data()[176]	4.050s	passed
indexOfSeqConcatFirst	data()[177]	4.065s	passed
indexOfSeqConcatSecond	data()[178]	4.076s	passed
indexOfSeqSub	data()[179]	3.930s	passed
div_zero	data()[17]	3.982s	passed
lenOfArray2seq	data()[180]	3.835s	passed
getAnyOfArray2seq	data()[181]	3.890s	passed
getOfArray2seq	data()[182]	3.960s	passed
getAnyOfNPermInv	data()[183]	3.882s	passed
seqNPermRange	data()[184]	4.003s	passed
seqPermTrans	data()[185]	3.856s	passed
seqPermRefl	data()[186]	3.864s	passed
seqPermSplit	data()[187]	3.871s	passed
seqNPermRight	data()[188]	4.154s	passed
seqPermFromSwap	data()[189]	3.988s	passed
divResZero1	data()[18]	3.923s	passed
seqPermTransAlt0	data()[190]	3.840s	passed
seqPermTransAlt1	data()[191]	3.920s	passed
seqPermTransAlt2	data()[192]	3.852s	passed
seqPermTransAlt3	data()[193]	3.872s	passed
seqPermForall	data()[194]	3.955s	passed
seqPermExists	data()[195]	3.866s	passed
schiffl_lemma_2	data()[196]	28.552s	passed
schiffl_thm_1	data()[197]	4.686s	passed
eqSameSeq	data()[198]	3.923s	passed
divResZero2	data()[19]	3.877s	passed
eqTermCut	data()[1]	4.826s	passed
divResOne1	data()[20]	4.009s	passed
divResOne2	data()[21]	4.057s	passed
div_cancel1	data()[22]	4.051s	passed
div_cancel2	data()[23]	3.936s	passed
divAddMultDenom	data()[24]	3.895s	passed
divMinus	data()[25]	4.004s	passed
divMinusDenom	data()[26]	3.990s	passed
divLeastDPos	data()[27]	3.848s	passed
divLeastDNeg	data()[28]	3.861s	passed
divGreatestDPos	data()[29]	3.988s	passed
equivAllRight	data()[2]	4.448s	passed
divGreatestDNeg	data()[30]	3.857s	passed
divIncreasingPos	data()[31]	3.959s	passed
divIncreasingNeg	data()[32]	3.913s	passed
jdiv_zero	data()[33]	4.219s	passed
jdivPulloutMinusNum	data()[34]	3.997s	passed
jdivPulloutMinusDenom	data()[35]	4.159s	passed
jdiv_uniquePosPos	data()[36]	4.085s	passed
jdiv_uniquePosNeg	data()[37]	4.147s	passed
jdiv_uniqueNegPos	data()[38]	4.347s	passed
jdiv_uniqueNegNeg	data()[39]	4.270s	passed
irrflConcrete1	data()[3]	4.514s	passed
jdivMultDenom1	data()[40]	4.092s	passed
jdivMultDenom2	data()[41]	3.833s	passed
mod_geZero	data()[42]	3.813s	passed
mod_lessDenom	data()[43]	3.861s	passed
jmod_NumPos	data()[44]	3.696s	passed
jmod_NumNeg	data()[45]	3.737s	passed
jmod_geZero	data()[46]	3.655s	passed
jmodNumZero	data()[47]	3.857s	passed
jmod_pulloutminusNum	data()[48]	3.794s	passed
jmod_pulloutminusDenom	data()[49]	3.734s	passed
irrflConcrete2	data()[4]	4.340s	passed
jmodUnique1	data()[50]	3.844s	passed
jmodUnique2	data()[51]	3.926s	passed
intDivRem	data()[52]	3.814s	passed
jmodjmod	data()[53]	3.966s	passed
jmodDivisible	data()[54]	3.993s	passed
jmodDivisibleRep	data()[55]	3.750s	passed
jdivAddMultDenom	data()[56]	4.039s	passed
jmodAltZero	data()[57]	3.877s	passed
jmodAddMultDenomZero	data()[58]	3.880s	passed
polyDiv_zero	data()[59]	3.797s	passed
cancel_gtPos	data()[5]	4.200s	passed
polyMod_ltdivDenom	data()[60]	3.750s	passed
bsum_empty	data()[61]	3.753s	passed
bsum_induction_upper	data()[62]	3.932s	passed
bsum_induction_lower	data()[63]	3.860s	passed
bsum_num_of_bounds	data()[64]	3.697s	passed
bsum_num_of_bounds2	data()[65]	3.745s	passed
bsum_induction_upper2	data()[66]	3.793s	passed
bsum_induction_upper_concrete	data()[67]	3.978s	passed
bsum_induction_upper_concrete_2	data()[68]	4.004s	passed
bsum_induction_upper2_concrete	data()[69]	3.850s	passed
cancel_gtNeg	data()[6]	4.126s	passed
bsum_induction_lower_concrete	data()[70]	3.751s	passed
bsum_induction_lower2	data()[71]	3.771s	passed
bsum_induction_lower2_concrete	data()[72]	3.736s	passed
bsum_positive	data()[73]	3.828s	passed
bsum_upper_bound	data()[74]	3.838s	passed
bsum_lower_bound	data()[75]	3.843s	passed
bsum_positive_lower_bound_element	data()[76]	3.800s	passed
bsum_sub_same_index	data()[77]	3.825s	passed
bsum_less_same_index	data()[78]	3.763s	passed
bsum_equal_except_one_index	data()[79]	3.856s	passed
moduloIntIsInInt	data()[7]	4.147s	passed
bsum_num_of_is_max	data()[80]	3.802s	passed
bsum_num_of_is_max2	data()[81]	3.838s	passed
bsum_num_of_is_max3	data()[82]	3.838s	passed
bsum_num_of_is_max4	data()[83]	3.866s	passed
bsum_num_of_lt_max	data()[84]	3.808s	passed
bsum_num_of_lt_max2	data()[85]	3.797s	passed
bsum_num_of_lt_max3	data()[86]	3.862s	passed
bsum_num_of_lt_max4	data()[87]	3.844s	passed
bsum_num_of_gt0	data()[88]	3.774s	passed
bsum_num_of_gt0_alt	data()[89]	3.753s	passed
moduloLongIsInLong	data()[8]	3.976s	passed
bsum_add_concrete	data()[90]	3.751s	passed
bprod_all_positive	data()[91]	3.918s	passed
bprod_split	data()[92]	3.788s	passed
powConcrete0	data()[93]	3.739s	passed
powConcrete1	data()[94]	3.713s	passed
powSplitFactor	data()[95]	3.740s	passed
powAdd	data()[96]	4.023s	passed
powMono	data()[97]	4.043s	passed
powMonoConcrete	data()[98]	3.811s	passed
powMonoConcreteRight	data()[99]	3.724s	passed
moduloShortIsInShort	data()[9]	4.103s	passed
Standard output

721        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
753        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 16.06ms 
1081       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1106       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)

2523       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2525       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2529       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2529       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4591       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11545      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.46s 
11664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11724      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40ns 
11744      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11744      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.21ns 
11749      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15316      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
15320      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16556      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.59ms 
16568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16569      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 692.12ns 
16571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19938      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
19938      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21014      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.96ms 
21016      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21017      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132ns 
21018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24464      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
24465      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25527      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
25533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25533      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440.52ns 
25535      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28805      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
28805      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
29852      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
29868      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.71ms 
29876      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
29876      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 562.22ns 
29880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32948      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
32948      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34004      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34073      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.89ms 
34076      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34077      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.01ns 
34078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37180      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
37181      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38173      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
38199      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.35ms 
38204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
38205      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 591.22ns 
38207      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41301      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
41302      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42342      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
42349      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
42351      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
42352      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.1ns 
42353      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
45339      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
46324      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 674.03ns 
46328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
46328      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.91ns 
46329      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49421      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
49423      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
50428      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 602.72ns 
50431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
50431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 477.62ns 
50433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53530      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
53531      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
54489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
54495      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717.83ns 
54498      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
54498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 507.32ns 
54499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57520      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
57521      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
58499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
58502      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.34ns 
58505      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
58505      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.72ns 
58507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
61517      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
62522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
62584      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.89ms 
62587      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
62588      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.71ns 
62589      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65569      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
65570      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
66511      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
66618      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.98ms 
66621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
66621      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.91ns 
66622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
69641      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
70598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
70816      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 207.1ms 
70820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
70821      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440.72ns 
70822      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73765      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
73766      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
74684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
74690      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
74692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
74693      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.41ns 
74694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77643      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
77644      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
78638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
78646      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
78650      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
78651      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 544.62ns 
78652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81627      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
81628      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
82559      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
82631      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.5ms 
82634      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
82634      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.11ns 
82636      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85570      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
85570      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
86533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
86555      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.09ms 
86556      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
86557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
86558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89478      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
89479      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
90412      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
90432      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.32ms 
90434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
90434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.31ns 
90435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93364      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
93364      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
94416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
94441      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.07ms 
94444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
94445      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.71ns 
94446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97509      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
97510      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
98476      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
98499      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.15ms 
98501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
98501      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.21ns 
98502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
101565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
102512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
102549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.7ms 
102552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
102553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.12ns 
102554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
105542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
106482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
106486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
106488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
106488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.51ns 
106489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
109388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
110318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
110381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.04ms 
110383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
110383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.11ns 
110384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
113320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
114290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
114385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.28ms 
114395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
114396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 845.03ns 
114398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
117332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
118306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
118375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.87ms 
118377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
118377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.7ns 
118378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
121284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
122212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
122223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.61ms 
122225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
122225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.1ns 
122227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
125141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
126065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
126084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.92ms 
126086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
126086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
126087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
129135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
130053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
130071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.04ms 
130075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
130075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.51ns 
130076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
132970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
133918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
133929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.25ms 
133931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
133931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
133932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
136924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
137877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
137888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.84ms 
137890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
137891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.41ns 
137892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
140820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
141791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
141801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.54ms 
141803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
141803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.5ns 
141804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
144865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
146015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
146020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
146023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
146023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.51ns 
146026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
149045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
149985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
150015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.18ms 
150019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
150019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.5ns 
150021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
153081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
154096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
154175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.68ms 
154190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
154191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 536.61ns 
154192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
157243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
158217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
158261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.38ms 
158265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
158265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.11ns 
158267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
161312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
162367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
162410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.76ms 
162411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
162411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.5ns 
162412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
165693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
166711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
166756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.09ms 
166757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
166757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
166758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
169956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
170995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
171025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.73ms 
171027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
171027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.41ns 
171028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
174105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
175050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
175118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.56ms 
175120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
175120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
175121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
178000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
178943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
178950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
178953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
178954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.81ns 
178955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
181788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
182757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
182764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.88ms 
182766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
182767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.51ns 
182767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
185714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
186613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
186625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.06ms 
186628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
186628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.51ns 
186629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
189419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
190310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
190322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.52ms 
190323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
190323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
190324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
193101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
194025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
194059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.12ms 
194063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
194063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.01ns 
194064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
196827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
197702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
197714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
197716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
197716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
197716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
200542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
201562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
201571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
201574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
201575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 795.32ns 
201576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
204459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
205360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
205366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
205367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
205367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
205368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
208166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
209094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
209099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
209101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
209101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
209102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
211910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
212823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
212943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.96ms 
212945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
212945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.51ns 
212946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
215813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
216730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
216868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127.47ms 
216871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
216871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.01ns 
216872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
219743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
220677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
220683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
220685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
220685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.11ns 
220686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
223612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
224573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
224649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.28ms 
224652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
224661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.19ms 
224662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
227647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
228585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
228642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.44ms 
228644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
228644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
228653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
231474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
232388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
232392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
232395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
232395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.71ns 
232396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
235257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
236186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
236432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 231.54ms 
236435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
236435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.31ns 
236436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
239331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
240293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
240310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.56ms 
240311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
240311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
240312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
243243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
244178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
244190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
244191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
244191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
244192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
247058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
247962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
247986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.43ms 
247987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
247987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
247988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
250824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
251717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
251735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.01ms 
251738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
251738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
251739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
254579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
255485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
255489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
255491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
255491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
255492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
258408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
259415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
259421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
259423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
259423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
259424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
262330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
263218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
263281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.85ms 
263283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
263283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
263284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
266077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
266955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
266978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.03ms 
266980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
266980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
266981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
269812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
270694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
270723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.56ms 
270725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
270725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
270726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
273582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
274512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
274516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
274518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
274518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
274519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
277501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
278488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
278494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
278496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
278496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
278496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
281570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
282491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
282499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
282500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
282500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.1ns 
282501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
285437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
286344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
286348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
286350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
286350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.21ns 
286351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
289205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
290097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
290099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 960.43ns 
290101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
290101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
290102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
292957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
293865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
293871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
293872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
293872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.2ns 
293873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
296725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
297604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
297607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
297608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
297608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
297609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
300422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
301365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
301434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.47ms 
301436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
301436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
301437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
304327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
305222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
305272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.93ms 
305274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
305274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
305275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
308138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
309061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
309115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.94ms 
309117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
309117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
309118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
311938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
312851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
312915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.83ms 
312917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
312917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
312918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
315792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
316691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
316740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.8ms 
316741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
316741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
316742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
319528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
320425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
320503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.9ms 
320506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
320506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.01ns 
320507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
323395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
324310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
324359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.89ms 
324361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
324361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.31ns 
324363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
327253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
328131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
328161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.63ms 
328162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
328162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
328165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
331044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
331961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
331999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.32ms 
332001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
332001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.21ns 
332002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
334850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
335807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
335838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.22ms 
335839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
335839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192ns 
335840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
338724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
339655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
339702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.8ms 
339704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
339705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
339705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
342527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
343470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
343511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.31ms 
343513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
343513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
343514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
346354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
347261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
347307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.46ms 
347309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
347309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
347310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
350187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
351130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
351170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.6ms 
351171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
351172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
351172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
354061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
354983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
355015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.4ms 
355017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
355017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
355017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
357839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
358753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
358789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.04ms 
358790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
358790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
358791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
361588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
362505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
362541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.31ms 
362543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
362543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
362543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
365379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
366278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
366292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.24ms 
366294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
366294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
366295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
369255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
370187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
370210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.76ms 
370212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
370212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
370213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
373051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
373993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
373998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
374000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
374000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.51ns 
374001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
376847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
377734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
377737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 904.62ns 
377739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
377740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.31ns 
377740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
380542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
381448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
381451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 908.42ns 
381453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
381453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
381454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
384243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
385172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
385190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.47ms 
385194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
385194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
385195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
388178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
389206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
389215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ms 
389216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
389217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
389217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
392367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
393241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
393258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.78ms 
393260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
393260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
393261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
396156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
397066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
397070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
397071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
397071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
397072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
399866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
400791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
400793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.02ns 
400795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
400795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
400796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
403692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
404641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
404648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ms 
404650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
404650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
404651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
407642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
408659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
408662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
408664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
408664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
408667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
411979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
413018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
413021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 933.03ns 
413022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
413022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
413023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
416094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
417075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
417077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 797.72ns 
417079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
417079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
417080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
419942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
420844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
420849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
420850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
420850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
420851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
423891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
424863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
424874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.41ms 
424875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
424876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
424876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
427823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
428804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
428809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
428810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
428810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
428811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
431765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
432699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
432709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ms 
432711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
432711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
432712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
435738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
436727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
436734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
436735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
436735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
436736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
439693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
440639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
440661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.92ms 
440662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
440662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.1ns 
440663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
443501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
444448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
444452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
444453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
444453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
444454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
447308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
448216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
448219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
448221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
448221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
448221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
451132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
452033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
452038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
452040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
452040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
452040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
454922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
455908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
455933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.63ms 
455936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
455936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.91ns 
455937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
458829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
459727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
459733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 723.52ns 
459736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
459736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.21ns 
459737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
462550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
463465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
463522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.83ms 
463523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
463524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
463524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
466350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
467261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
467266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
467267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
467267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
467268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
470121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
471058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
471095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.63ms 
471097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
471097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
471097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
474089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
475022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
475052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.48ms 
475054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
475054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
475055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
478034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
479041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
479077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32ms 
479079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
479079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
479079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
482161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
483208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
483211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 697.22ns 
483212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
483212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
483213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
486182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
487080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
487088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
487089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
487089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
487090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
489920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
490861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
490864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
490866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
490866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
490867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
493700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
494630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
494633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
494635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
494635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
494635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
497530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
498526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
498529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
498530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
498530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
498531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
501441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
502372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
502375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
502377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
502377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
502378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
505364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
506332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
506335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
506337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
506337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
506337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
509268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
510202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
510216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.51ms 
510217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
510217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
510218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
513020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
513970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
513986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms 
513987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
513987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
513988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
516864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
517775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
517790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.63ms 
517792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
517792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
517792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
520607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
521540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
521556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.69ms 
521557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
521557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
521558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
524431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
525407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
525413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
525414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
525415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
525415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
528409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
529427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
529435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.15ms 
529436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
529436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
529437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
532416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
533391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
533393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.73ns 
533395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
533395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
533395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
536257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
537204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
537208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
537210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
537211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.81ns 
537211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
540213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
541179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
541182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
541183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
541183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
541184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
544185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
545240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
545256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms 
545258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
545261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.13ms 
545262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
548233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
549187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
549192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
549194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
549194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
549195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
552029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
552956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
552965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.81ms 
552966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
552966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
552967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
555850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
556830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
556833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 926.83ns 
556835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
556835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
556835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
559791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
560764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
560767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 890.23ns 
560768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
560768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
560769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
563767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
564737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
564745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
564747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
564747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
564748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
567536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
568460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
568463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
568465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
568465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
568466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
571314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
572248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
572251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
572252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
572253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
572254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
575117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
576112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
576115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
576117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
576117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
576117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
579002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
579932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
579940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.14ms 
579941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
579941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
579942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
582771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
583713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
583716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
583718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
583718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
583719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
586585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
587526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
587542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.55ms 
587543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
587543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
587544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
590428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
591364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
591368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
591369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
591369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
591370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
594238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
595198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
595208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ms 
595210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
595210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.41ns 
595211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
598109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
599098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
599101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
599104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
599104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
599104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
601933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
602892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
602894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
602895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
602895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
602896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
605775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
606730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
606737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
606739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
606739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
606739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
609709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
610660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
610664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
610666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
610666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
610667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
613489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
614458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
614462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
614463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
614463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
614464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
617269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
618217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
618222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
618226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
618226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
618227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
621131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
622071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
622079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
622080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
622080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
622081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
625057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
625996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
626016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.98ms 
626017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
626017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
626018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
628871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
629811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
629836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.32ms 
629837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
629837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
629838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
632739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
633760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
633774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.47ms 
633775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
633775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
633776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
636827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
637804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
637818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.41ms 
637820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
637820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
637821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
640729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
641673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
641712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.03ms 
641713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
641713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
641714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
644551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
645518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
645553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.32ms 
645555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
645555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
645555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
648475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
649426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
649458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.5ms 
649460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
649460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
649460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
652332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
653269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
653289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.67ms 
653290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
653290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
653291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
656285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
657246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
657320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.47ms 
657323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
657323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.2ns 
657324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
660179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
661137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
661206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.18ms 
661207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
661207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
661208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
664193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
665126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
665178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.84ms 
665180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
665180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
665181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
668032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
668997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
669056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.13ms 
669058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
669058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
669059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
671973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
672931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
672994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.66ms 
672995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
672996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
672997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
675945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
676939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
677107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 160.12ms 
677109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
677109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
677110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
679979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
680922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
680936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
680938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
680938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
680938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
683857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
684808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
684818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.05ms 
684819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
684820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
684820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
687713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
688666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
688672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.78ms 
688674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
688674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
688674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
691545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
692490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
692516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.85ms 
692518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
692518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
692519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
695425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
696408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
696423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.63ms 
696424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
696424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
696425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
699469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
700466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
700472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
700473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
700473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
700474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
703491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
704513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
704537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.45ms 
704539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
704539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
704540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
707577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
708591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
708613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.52ms 
708615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
708615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
708616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
711542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
712515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
712543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.54ms 
712546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
712546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
712546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
715466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
716375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
716378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
716380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
716380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
716381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
719283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
720264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
720269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
720270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
720270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
720271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
723220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
724219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
724229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.36ms 
724230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
724230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
724231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
727136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
728102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
728110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.39ms 
728112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
728112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
728113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
730991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
731981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
732112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 125.16ms 
732115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
732115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.91ns 
732116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
734967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
735932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
735969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.33ms 
735971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
735971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
735972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
738840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
739803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
739833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.51ms 
739835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
739835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
739836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
742747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
743701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
743704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 332.61ns 
743706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
743706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.41ns 
743707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
746596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
747576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
747858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 269.28ms 
747860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
747860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
747861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
750782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
751746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
751846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 95.93ms 
751848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
751848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
751849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
754710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
755684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
755686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 459.31ns 
755688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
755688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
755688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
758617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
759604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
759606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 471.01ns 
759607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
759607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
759608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
762519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
763456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
763458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 426.01ns 
763460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
763461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.37ms 
763462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
766374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
767328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
767330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703.22ns 
767331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
767332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
767332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
770191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
771142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
771285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 140.24ms 
771287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
771288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.71ns 
771289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
774132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
775098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
775152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.72ms 
775153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
775153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
775155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
778014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
779030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
779033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
779080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
779119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
779139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
779145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
779152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
779155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
779160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
779163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
779168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
779173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
779178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
779182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
779468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
779470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
779471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
779473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
779474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
779645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
779646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
779650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
779652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
779653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
779654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
779911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
779914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
779915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
779916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
779916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
779922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
780103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
780105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
780106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
780107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
780107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
780108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
780119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
780120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
780121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
780123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
780126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
780126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
780138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
780139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
780141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
780142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
780143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
780144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
780360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
780362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
780365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
780529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
780531     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)'' 
780534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
780535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
780537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
780538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
780539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
780542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
780547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
780548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
780549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
780550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
780551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
780699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
780704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
780705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
780706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
780707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
780708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
780710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
780880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
780884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
780885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
780889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
780890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
780891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
780892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
780895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
781039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
781041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
781242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
781251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
781258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
781259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
781260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
781262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
781265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
781265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
781266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
781267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
781278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
781284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
781414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
781416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
781418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
781419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
781420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
781420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
781421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
781422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
781495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
781502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
781680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
781681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
781683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
781684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
781685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
781686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
781879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
781885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
781886     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)'' 
781888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
781889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
781890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
781890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
781891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
781903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
781904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
781906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
781906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
782048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
782050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
782051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
782051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
782052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
782053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
782190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
782191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
782192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
782194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
782195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
782196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
782196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
782198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
782309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
782310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
782407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
782408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
782409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
782415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
782420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
782425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
782577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
782579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
782580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
782581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
782593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
782694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
787108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
787109     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)'' 
787114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
787115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
787116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
787116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
787118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
787129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
787130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
787132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
787133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
787133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
787253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
787258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
787259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
787260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
787261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
787262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
787262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
787455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
787457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
787457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
787460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
787461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
787461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
787462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
787463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
787558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
787559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
787668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
787673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
787678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
787679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
787680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
787682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
787697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
787812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
787814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
787815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
787816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
787911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
787921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
787922     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)'' 
787924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
787925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
787926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
787926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
787927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
787945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
787947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
787948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
787948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
787949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
788057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
788058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
788060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
788060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
788061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
788178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
788185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
788187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
788188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
788188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
788189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
788190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
788314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
788316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
788317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
788319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
788319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
788320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
788321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
788325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
788326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
788327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
788328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
788328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
788329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
788329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
788330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
788444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
788445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
788454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
788555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
788658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
788660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
788661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
788662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
788663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
788663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
788664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
788664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
788665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
788775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
788783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
788889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
788890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
788891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
788892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
788893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
788893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
788893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
788894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
788900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
788901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
789010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
789017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
789023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
789155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
789156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
789157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
789158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
789159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
789159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
789159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
789160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
789230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
789231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
789232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
789233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
789234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
789240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
789248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
789451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
789558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
789559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
789560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
789561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
789772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
789874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
789875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
793570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
793576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
793577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
793578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
793578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
793718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
793720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
793721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
793722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
793723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
793864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
797901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
802068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
802074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
802075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
802075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
802076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
802220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
802222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
802223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
802224     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)' ...' 
802227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
803706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
803706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.91ns 
803707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
806671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
806671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
807647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
807648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
807649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
807655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
807668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
807671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
807673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
807673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
807677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
807679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
807682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
807685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
807686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
807696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
807698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
807698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
807754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
807755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
807756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
807757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
807757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
807830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
807830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
807832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
807833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
807833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
807837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
807838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
807839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
807840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
807841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
807842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
807929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
807930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
807931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
807932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
807933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
807934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
808018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
808019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
808020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
808021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
808021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
808023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
808023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
808024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
808026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
808027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
808027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
808028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
808028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
808029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
808029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
808030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
808031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
808032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
808033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
808036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
808073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
808075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
808128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
808130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
808132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
808134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
808135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
808135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
808186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
808189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
808191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
808197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
808199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
808200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
808200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
808253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
808257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
808261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
808324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
808391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
808392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.11ns 
808393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
811241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
811242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
812254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
812311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.57ms