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

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

Test	Method name	Duration	Result
powPositive	data()[100]	4.286s	passed
powPositiveConcrete	data()[101]	4.285s	passed
powGeq1Concrete	data()[102]	4.371s	passed
pow2InIntLower	data()[103]	4.474s	passed
pow2InIntUpper	data()[104]	4.307s	passed
logSelfConcrete	data()[105]	4.357s	passed
log1Concrete	data()[106]	4.515s	passed
logProduct	data()[107]	4.367s	passed
logTimesBaseConcrete	data()[108]	4.380s	passed
logProdIdentity	data()[109]	4.402s	passed
moduloByteIsInByte	data()[10]	4.459s	passed
logProdIdentityConcrete	data()[110]	4.364s	passed
logPowIdentity	data()[111]	4.523s	passed
logPowIdentityConcrete	data()[112]	4.357s	passed
logPositive	data()[113]	4.357s	passed
logPositiveConcrete	data()[114]	4.334s	passed
logMono	data()[115]	4.418s	passed
logMonoConcrete	data()[116]	4.425s	passed
powLogLess	data()[117]	4.536s	passed
powLogMore2	data()[118]	4.351s	passed
logLessThanPow	data()[119]	4.393s	passed
moduloCharIsInChar	data()[11]	4.320s	passed
logLessThanPowConcrete	data()[120]	4.520s	passed
logSqueeze	data()[121]	4.490s	passed
ifthenelse_equals	data()[122]	4.443s	passed
ifthenelse_equals_1	data()[123]	4.496s	passed
ifthenelse_equals_2	data()[124]	4.386s	passed
disjointWithSingleton1	data()[125]	4.406s	passed
disjointWithSingleton2	data()[126]	4.411s	passed
disjointArrayRanges	data()[127]	4.498s	passed
disjointArrayRangeAllFields1	data()[128]	4.454s	passed
disjointArrayRangeAllFields2	data()[129]	4.440s	passed
div_unique1	data()[12]	4.608s	passed
seqSelfDefinition	data()[130]	4.591s	passed
seqOutsideValue	data()[131]	4.266s	passed
castedGetAny	data()[132]	4.384s	passed
seqGetAlphaCast	data()[133]	4.429s	passed
getOfSeqSingleton	data()[134]	4.424s	passed
getOfSeqSingletonConcrete	data()[135]	4.412s	passed
getOfSeqConcat	data()[136]	4.413s	passed
getOfSeqSub	data()[137]	4.449s	passed
getOfSeqReverse	data()[138]	4.535s	passed
lenOfSeqEmpty	data()[139]	4.417s	passed
div_unique2	data()[13]	4.508s	passed
lenOfSeqSingleton	data()[140]	4.412s	passed
lenOfSeqConcat	data()[141]	4.429s	passed
lenOfSeqSub	data()[142]	4.375s	passed
lenOfSeqReverse	data()[143]	4.460s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	4.420s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	4.296s	passed
getOfSeqSingletonEQ	data()[146]	4.319s	passed
getOfSeqConcatEQ	data()[147]	4.439s	passed
getOfSeqSubEQ	data()[148]	4.371s	passed
getOfSeqReverseEQ	data()[149]	4.251s	passed
div_exists	data()[14]	4.740s	passed
lenOfSeqEmptyEQ	data()[150]	4.375s	passed
lenOfSeqSingletonEQ	data()[151]	4.238s	passed
lenOfSeqConcatEQ	data()[152]	4.248s	passed
lenOfSeqSubEQ	data()[153]	4.236s	passed
lenOfSeqReverseEQ	data()[154]	4.290s	passed
getOfSeqDefEQ	data()[155]	4.368s	passed
lenOfSeqDefEQ	data()[156]	4.343s	passed
seqConcatWithSeqEmpty1	data()[157]	4.334s	passed
seqConcatWithSeqEmpty2	data()[158]	4.507s	passed
seqReverseOfSeqEmpty	data()[159]	4.320s	passed
div_one	data()[15]	4.478s	passed
subSeqComplete	data()[160]	4.260s	passed
subSeqTailR	data()[161]	4.246s	passed
subSeqTailL	data()[162]	4.396s	passed
subSeqTailEQR	data()[163]	4.399s	passed
subSeqTailEQL	data()[164]	4.435s	passed
seqDef_split	data()[165]	4.437s	passed
seqDef_induction_upper	data()[166]	4.490s	passed
seqDef_induction_upper_concrete	data()[167]	4.438s	passed
seqDef_induction_lower	data()[168]	4.500s	passed
seqDef_induction_lower_concrete	data()[169]	4.453s	passed
jdiv_one	data()[16]	4.618s	passed
seqDef_split_in_three	data()[170]	4.508s	passed
seqDef_empty	data()[171]	4.457s	passed
seqDef_one_summand	data()[172]	4.312s	passed
seqDef_lower_equals_upper	data()[173]	4.323s	passed
seqDefOfSeq	data()[174]	4.364s	passed
seqSelfDefinitionEQ2	data()[175]	4.351s	passed
indexOfSeqSingleton	data()[176]	4.327s	passed
indexOfSeqConcatFirst	data()[177]	4.244s	passed
indexOfSeqConcatSecond	data()[178]	4.275s	passed
indexOfSeqSub	data()[179]	4.201s	passed
div_zero	data()[17]	4.549s	passed
lenOfArray2seq	data()[180]	4.220s	passed
getAnyOfArray2seq	data()[181]	4.222s	passed
getOfArray2seq	data()[182]	4.221s	passed
getAnyOfNPermInv	data()[183]	4.231s	passed
seqNPermRange	data()[184]	4.346s	passed
seqPermTrans	data()[185]	4.576s	passed
seqPermRefl	data()[186]	4.317s	passed
seqPermSplit	data()[187]	4.405s	passed
seqNPermRight	data()[188]	4.696s	passed
seqPermFromSwap	data()[189]	4.680s	passed
divResZero1	data()[18]	4.554s	passed
seqPermTransAlt0	data()[190]	4.437s	passed
seqPermTransAlt1	data()[191]	4.257s	passed
seqPermTransAlt2	data()[192]	4.298s	passed
seqPermTransAlt3	data()[193]	4.366s	passed
seqPermForall	data()[194]	4.458s	passed
seqPermExists	data()[195]	4.516s	passed
schiffl_lemma_2	data()[196]	28.013s	passed
schiffl_thm_1	data()[197]	5.235s	passed
eqSameSeq	data()[198]	4.544s	passed
divResZero2	data()[19]	4.327s	passed
eqTermCut	data()[1]	5.317s	passed
divResOne1	data()[20]	4.433s	passed
divResOne2	data()[21]	4.424s	passed
div_cancel1	data()[22]	4.604s	passed
div_cancel2	data()[23]	4.524s	passed
divAddMultDenom	data()[24]	4.559s	passed
divMinus	data()[25]	4.566s	passed
divMinusDenom	data()[26]	4.510s	passed
divLeastDPos	data()[27]	4.541s	passed
divLeastDNeg	data()[28]	4.412s	passed
divGreatestDPos	data()[29]	4.479s	passed
equivAllRight	data()[2]	5.149s	passed
divGreatestDNeg	data()[30]	4.391s	passed
divIncreasingPos	data()[31]	4.516s	passed
divIncreasingNeg	data()[32]	4.483s	passed
jdiv_zero	data()[33]	4.324s	passed
jdivPulloutMinusNum	data()[34]	4.397s	passed
jdivPulloutMinusDenom	data()[35]	4.470s	passed
jdiv_uniquePosPos	data()[36]	4.481s	passed
jdiv_uniquePosNeg	data()[37]	4.341s	passed
jdiv_uniqueNegPos	data()[38]	4.291s	passed
jdiv_uniqueNegNeg	data()[39]	4.429s	passed
irrflConcrete1	data()[3]	4.790s	passed
jdivMultDenom1	data()[40]	4.490s	passed
jdivMultDenom2	data()[41]	4.621s	passed
mod_geZero	data()[42]	4.691s	passed
mod_lessDenom	data()[43]	4.518s	passed
jmod_NumPos	data()[44]	4.518s	passed
jmod_NumNeg	data()[45]	4.542s	passed
jmod_geZero	data()[46]	4.578s	passed
jmodNumZero	data()[47]	4.716s	passed
jmod_pulloutminusNum	data()[48]	4.551s	passed
jmod_pulloutminusDenom	data()[49]	4.720s	passed
irrflConcrete2	data()[4]	4.688s	passed
jmodUnique1	data()[50]	4.718s	passed
jmodUnique2	data()[51]	4.779s	passed
intDivRem	data()[52]	4.524s	passed
jmodjmod	data()[53]	4.739s	passed
jmodDivisible	data()[54]	4.689s	passed
jmodDivisibleRep	data()[55]	4.714s	passed
jdivAddMultDenom	data()[56]	4.905s	passed
jmodAltZero	data()[57]	4.717s	passed
jmodAddMultDenomZero	data()[58]	4.616s	passed
polyDiv_zero	data()[59]	4.376s	passed
cancel_gtPos	data()[5]	4.810s	passed
polyMod_ltdivDenom	data()[60]	4.433s	passed
bsum_empty	data()[61]	4.205s	passed
bsum_induction_upper	data()[62]	4.353s	passed
bsum_induction_lower	data()[63]	4.432s	passed
bsum_num_of_bounds	data()[64]	4.366s	passed
bsum_num_of_bounds2	data()[65]	4.262s	passed
bsum_induction_upper2	data()[66]	4.225s	passed
bsum_induction_upper_concrete	data()[67]	4.313s	passed
bsum_induction_upper_concrete_2	data()[68]	4.188s	passed
bsum_induction_upper2_concrete	data()[69]	4.365s	passed
cancel_gtNeg	data()[6]	4.533s	passed
bsum_induction_lower_concrete	data()[70]	4.190s	passed
bsum_induction_lower2	data()[71]	4.402s	passed
bsum_induction_lower2_concrete	data()[72]	4.567s	passed
bsum_positive	data()[73]	4.540s	passed
bsum_upper_bound	data()[74]	4.618s	passed
bsum_lower_bound	data()[75]	4.569s	passed
bsum_positive_lower_bound_element	data()[76]	4.685s	passed
bsum_sub_same_index	data()[77]	4.537s	passed
bsum_less_same_index	data()[78]	4.457s	passed
bsum_equal_except_one_index	data()[79]	4.552s	passed
moduloIntIsInInt	data()[7]	4.542s	passed
bsum_num_of_is_max	data()[80]	4.390s	passed
bsum_num_of_is_max2	data()[81]	4.264s	passed
bsum_num_of_is_max3	data()[82]	4.394s	passed
bsum_num_of_is_max4	data()[83]	4.357s	passed
bsum_num_of_lt_max	data()[84]	4.429s	passed
bsum_num_of_lt_max2	data()[85]	4.546s	passed
bsum_num_of_lt_max3	data()[86]	4.581s	passed
bsum_num_of_lt_max4	data()[87]	4.590s	passed
bsum_num_of_gt0	data()[88]	4.287s	passed
bsum_num_of_gt0_alt	data()[89]	4.367s	passed
moduloLongIsInLong	data()[8]	4.521s	passed
bsum_add_concrete	data()[90]	4.302s	passed
bprod_all_positive	data()[91]	4.232s	passed
bprod_split	data()[92]	4.225s	passed
powConcrete0	data()[93]	4.372s	passed
powConcrete1	data()[94]	4.247s	passed
powSplitFactor	data()[95]	4.270s	passed
powAdd	data()[96]	4.262s	passed
powMono	data()[97]	4.345s	passed
powMonoConcrete	data()[98]	4.255s	passed
powMonoConcreteRight	data()[99]	4.357s	passed
moduloShortIsInShort	data()[9]	4.645s	passed
Standard output

422        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
448        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.81ms 
717        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734        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)

1803       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1805       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1809       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1809       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3739       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10861      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.14s 
10939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10988      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.8ns 
11008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11009      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.59ms 
11015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14956      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 
14959      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16271      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16310      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.86ms 
16325      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16325      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.7ns 
16327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20115      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
20116      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21469      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.63ms 
21474      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21475      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 437.7ns 
21480      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25123      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
25123      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
26239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
26260      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.06ms 
26267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
26267      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 689.4ns 
26270      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29803      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
29804      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30944      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30951      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
30954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30955      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 473.3ns 
30956      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34456      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
34457      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
35678      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
35762      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.58ms 
35767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
35768      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.6ns 
35769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39126      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
39127      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
40238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
40294      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.94ms 
40298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
40299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.6ns 
40300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43731      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
43732      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
44831      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
44836      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 859.61ns 
44839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
44840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.2ns 
44841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48218      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
48219      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
49352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
49357      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 798.6ns 
49361      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
49361      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.6ns 
49363      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
52917      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
54001      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
54004      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 616.5ns 
54007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
54008      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 436.8ns 
54009      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57390      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
57390      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
58460      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
58464      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 902.8ns 
58467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
58468      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.3ns 
58469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61773      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
61774      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
62780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
62783      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 668.2ns 
62787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
62787      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.3ns 
62788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66175      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
66176      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
67318      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
67389      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.1ms 
67406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
67407      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 716.7ns 
67409      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70741      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
70742      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
71851      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
71907      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.19ms 
71913      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
71913      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433ns 
71915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75233      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
75233      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
76306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
76646      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 329.72ms 
76651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
76651      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.4ns 
76653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80042      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
80042      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
81118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
81127      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
81130      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
81130      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.8ns 
81132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84630      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
84631      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
85742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
85746      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
85749      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
85749      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.1ns 
85750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
89159      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
90236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
90295      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.11ms 
90298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
90299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 418.4ns 
90300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93758      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
93759      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
94825      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
94849      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.66ms 
94853      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
94853      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.9ns 
94855      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98090      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
98091      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
99156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
99176      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.78ms 
99180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
99180      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 482.1ns 
99182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
102489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
103587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
103609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.15ms 
103613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
103613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.1ns 
103614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
106952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
107962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
108033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.39ms 
108037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
108040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.37ms 
108041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
111492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
112600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
112638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.91ms 
112642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
112642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 431.7ns 
112643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
116090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
117159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
117163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
117165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
117165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
117166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
120603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
121659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
121722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.7ms 
121724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
121724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
121726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
125084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
126185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
126287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.84ms 
126291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
126291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.7ns 
126292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
129619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
130727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
130798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.69ms 
130799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
130799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
130801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
134234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
135328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
135339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.95ms 
135340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
135341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.7ns 
135342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
138660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
139726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
139749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.27ms 
139762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
139763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.35ms 
139765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
143136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
144221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
144237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.44ms 
144240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
144240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.4ns 
144242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
147574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
148618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
148629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.35ms 
148632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
148632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.6ns 
148633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
152022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
153128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
153143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.57ms 
153148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
153148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.3ns 
153149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
156527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
157619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
157628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.88ms 
157630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
157630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
157631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
160898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
161943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
161952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.84ms 
161954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
161954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.2ns 
161955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
165289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
166334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
166349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.28ms 
166351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
166351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201ns 
166353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
169640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
170740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
170818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.48ms 
170821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
170822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.1ns 
170823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
174213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
175267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
175300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.36ms 
175303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
175304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.3ns 
175305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
178570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
179614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
179642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.8ms 
179645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
179645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.2ns 
179646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
182885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
183907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
183932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.75ms 
183935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
183935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306ns 
183937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
187306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
188336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
188361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.27ms 
188363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
188364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
188365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
191651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
192788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
192851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.56ms 
192854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
192854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.1ns 
192856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
196294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
197469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
197473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
197475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
197476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.6ns 
197477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
201067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
202158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
202164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.96ms 
202166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
202166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
202167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
205583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
206670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
206683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.82ms 
206684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
206684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142ns 
206686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
210095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
211189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
211200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.02ms 
211202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
211202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
211203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
214614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
215710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
215742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.47ms 
215744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
215744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.5ns 
215745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
219159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
220301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
220320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.26ms 
220331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
220331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.6ns 
220333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
223863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
225034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
225038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
225041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
225041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.6ns 
225042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
228522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
229583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
229589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
229591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
229591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
229592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 
233171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
234302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
234309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
234312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
234312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.8ns 
234313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
237741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
238854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
239026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 161.87ms 
239030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
239030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.4ns 
239032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 
242576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
243672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
243806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 123.55ms 
243809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
243809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.1ns 
243810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
247204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
248326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
248331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
248333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
248334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.3ns 
248335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
251864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
253006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
253069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.06ms 
253072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
253073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 465.3ns 
253074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
256556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
257715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
257759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.86ms 
257761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
257761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
257762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
261312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
262468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
262473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
262475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
262475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.1ns 
262477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 
266021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
267136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
267378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.5ms 
267380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
267380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
267388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
270952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
272078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
272095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.54ms 
272099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
272099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
272100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
275524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
276677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
276712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.45ms 
276715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
276716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.5ns 
276717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
279950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
281064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
281089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.21ms 
281091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
281091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
281092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
284443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
285500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
285521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.01ms 
285525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
285525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
285526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
288711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
289721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
289727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
289728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
289729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
289729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
293004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
294073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
294080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
294082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
294082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
294084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
297462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
298478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
298512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.8ms 
298513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
298513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
298514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
301806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
302852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
302877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.43ms 
302879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
302880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.2ns 
302881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
306071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
307112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
307140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.87ms 
307142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
307142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.3ns 
307143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
310372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
311360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
311365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
311366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
311366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
311367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
314643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
315672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
315678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
315679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
315679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
315680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
318821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
319858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
319866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.68ms 
319868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
319868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
319868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
323208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
324226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
324231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
324233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
324233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
324234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
327426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
328418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
328421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
328423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
328423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.2ns 
328424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
331692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
332816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
332823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
332825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
332825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
332826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
336311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
337386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
337390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
337392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
337392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
337393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
340766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
341850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
341930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.03ms 
341933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
341933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221ns 
341934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
345380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
346486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
346548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.2ms 
346550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
346551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.6ns 
346552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
349950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
351047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
351117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.75ms 
351121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
351122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.3ns 
351123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
354629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
355730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
355802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.12ms 
355804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
355805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.5ns 
355806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
359159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
360286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
360339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.03ms 
360341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
360341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.5ns 
360342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
363645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
364710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
364796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.74ms 
364798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
364798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.5ns 
364799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
368223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
369304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
369348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.52ms 
369350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
369350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
369351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
372640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
373702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
373738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.56ms 
373739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
373740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
373740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
376962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
377964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
378002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.05ms 
378004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
378004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
378005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
381308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
382366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
382396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.16ms 
382399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
382399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.6ns 
382400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
385663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
386711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
386753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.72ms 
386755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
386755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
386756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
390091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
391136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
391181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.04ms 
391185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
391189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 497.6ns 
391193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
394537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
395663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
395727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.1ms 
395730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
395731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.7ns 
395732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
399137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
400266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
400309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.05ms 
400311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
400311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
400312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
403775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
404817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
404899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.92ms 
404901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
404901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns 
404902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
408160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
409146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
409186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.85ms 
409187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
409188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.6ns 
409188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
412437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
413514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
413553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.29ms 
413555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
413555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
413555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
416802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
417842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
417855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
417857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
417857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
417858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
421056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
422061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
422087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.45ms 
422089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
422089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
422090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
425258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
426307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
426312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
426313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
426313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
426314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
429634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
430680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
430684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 934.9ns 
430685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
430685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
430686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
433879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
434928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
434931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
434933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
434933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
434933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
438140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
439191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
439201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.55ms 
439203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
439203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
439204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
442420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
443455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
443463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.86ms 
443472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
443473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.1ns 
443474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
446715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
447790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
447808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.62ms 
447810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
447810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.8ns 
447811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
451007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
452059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
452063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
452065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
452065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
452066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
455359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
456417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
456421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.7ns 
456423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
456423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.7ns 
456424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
459660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
460699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
460706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
460708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
460708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
460709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
463917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
464988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
464991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 897.11ns 
464993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
464993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
464993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
468295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
469323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
469361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811.3ns 
469364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
469364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
469365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
472738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
473833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
473836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 838.1ns 
473838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
473838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
473839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
477095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
478138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
478143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
478145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
478145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
478146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
481437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
482485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
482500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ms 
482501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
482501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
482502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
485916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
487010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
487015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
487017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
487017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 448.9ns 
487018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
490322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
491372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
491382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.44ms 
491385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
491385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
491386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
494680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
495757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
495763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
495764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
495764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
495766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
499070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
500143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
500165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.19ms 
500167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
500167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
500168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
503455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
504524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
504529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
504531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
504531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
504532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
507888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
509041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
509052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.99ms 
509055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
509056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 782.8ns 
509057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
512340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
513404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
513409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
513411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
513411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
513412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
516695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
517739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
517766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.69ms 
517767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
517767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
517768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
521022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
522093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
522099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 732.9ns 
522101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
522101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
522102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
525363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
526464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
526518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.96ms 
526520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
526520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
526521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
529801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
530938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
530943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
530945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
530945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
530946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
534385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
535446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
535479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.6ms 
535481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
535482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.9ns 
535483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
538758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
539802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
539830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.66ms 
539832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
539832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
539833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
543135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
544188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
544223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.1ms 
544225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
544225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
544225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
547651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
548740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
548743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.6ns 
548744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
548744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
548745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
552130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
553226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
553233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.62ms 
553235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
553235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
553236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
556582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
557672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
557676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
557677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
557678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
557678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
561074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
562167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
562172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
562174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
562174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
562175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
565477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
566555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
566558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
566560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
566560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183ns 
566561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
569898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
570959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
570964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
570966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
570966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
570967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
574294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
575370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
575375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
575379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
575379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.8ns 
575380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
578754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
579861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
579874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.76ms 
579876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
579876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
579877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
583233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
584310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
584328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.69ms 
584330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
584330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
584330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
587707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
588751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
588767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.05ms 
588769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
588769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
588770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
592197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
593315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
593359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.55ms 
593361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
593362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.2ns 
593363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
596551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
597620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
597626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
597627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
597627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.9ns 
597628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
600950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
602001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
602009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.16ms 
602011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
602011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
602011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
605372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
606435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
606438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
606439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
606439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
606440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
609775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
610858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
610862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
610863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
610864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
610864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
614208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
615271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
615274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
615276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
615276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.1ns 
615277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
618571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
619670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
619687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.53ms 
619689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
619689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
619690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
623034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
624129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
624136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
624137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
624138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
624138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
627552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
628662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
628671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.84ms 
628673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
628673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
628674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
632001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
633085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
633088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
633089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
633090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
633091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
636425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
637497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
637500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 991.11ns 
637502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
637502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
637502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
640824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
641923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
641929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
641931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
641931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.5ns 
641932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
645202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
646300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
646304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
646306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
646306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 
646308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
649652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
650760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
650764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
650766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
650766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
650767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
654152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
655180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
655184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
655185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
655186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
655186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
658431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
659469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
659480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.14ms 
659482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
659482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
659482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
662728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
663794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
663799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
663801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
663801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
663802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
667061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
668223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
668238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.76ms 
668240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
668240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
668241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
671502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
672606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
672609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 879.61ns 
672611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
672611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
672612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
675799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
676850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
676860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.29ms 
676861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
676862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
676862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
680153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
681232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
681235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
681236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
681237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
681237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
684431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
685471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
685474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
685475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
685475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
685476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
688651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
689714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
689721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
689723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
689723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
689724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
692900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
693953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
693957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
693959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
693959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
693960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
697149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
698242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
698247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
698249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
698249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
698250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
701523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
702610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
702615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms 
702617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
702617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
702618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
705921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
706951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
706958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
706959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
706959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.2ns 
706960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
710145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
711270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
711292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.78ms 
711294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
711294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
711295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
714703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
715778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
715799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.84ms 
715801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
715801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
715802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
719060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
720105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
720119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.63ms 
720121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
720121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
720122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
723349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
724365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
724379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.68ms 
724380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
724381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
724381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
727536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
728587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
728625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.51ms 
728626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
728626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
728627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
731877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
732985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
733021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.28ms 
733022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
733022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
733023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
736325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
737387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
737420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.12ms 
737422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
737422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
737423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
740754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
741836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
741855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.33ms 
741857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
741857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
741858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
745189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
745189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
746250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
746292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.13ms 
746294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
746294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
746295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
749599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
750714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
750782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.15ms 
750784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
750784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
750785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
754082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
755155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
755220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.38ms 
755222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
755222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
755222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
758584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
759662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
759720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.16ms 
759721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
759721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
759722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
763006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
764113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
764172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.71ms 
764174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
764174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
764175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
767424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
768517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
768681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 155.35ms 
768682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
768683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
768683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
771992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
773127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
773138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.76ms 
773140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
773140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
773141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
776376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
777440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
777451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
777453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
777453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
777454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
780717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
781766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
781773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.29ms 
781774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
781774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
781775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
784999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
786105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
786137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.03ms 
786139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
786139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
786140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
789412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
790473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
790488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.36ms 
790490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
790490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
790491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
793733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
793733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
794811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
794815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
794816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
794817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
794817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
797989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
797989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
799037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
799059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.49ms 
799061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
799061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
799061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
802278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
802278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
803312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
803334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.55ms 
803335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
803335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
803336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
806479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
806480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
807510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
807535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.29ms 
807537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
807537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
807538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
810723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
810723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
811752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
811756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
811757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
811757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
811758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
814905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
814905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
815972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
815977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
815978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
815978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
815979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
819141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
819141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
820190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
820198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
820200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
820200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
820201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
823397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
824421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
824429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.06ms 
824430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
824430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
824431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
827611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
827611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
828677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
828775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.52ms 
828777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
828777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
828778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
832165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
832165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
833309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
833351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.35ms 
833353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
833353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.3ns 
833354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
836591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
836591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
837637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
837669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.55ms 
837673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
837673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.8ns 
837675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
840954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
840954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
842070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
842073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 394.3ns 
842076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
842076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.5ns 
842078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
845325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
845325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
846455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
846770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 302.13ms 
846772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
846772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.9ns 
846773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
850281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
850282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
851360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
851450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.05ms 
851452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
851452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.2ns 
851453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
854814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
854815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
855885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
855887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 498.9ns 
855892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
855892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
855893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
859066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
859066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
860144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
860147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 550.5ns 
860148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
860148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
860149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
863400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
863401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
864441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
864444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 459.6ns 
864445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
864445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
864446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
867734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
867734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
868807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
868810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703.5ns 
868812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
868812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
868812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
872062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
872062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
873150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
873249     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
873268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.67ms 
873270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
873271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.6ns 
873272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
876663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
876663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
877717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
877782     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
877784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.42ms 
877786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
877786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
877795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
881068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
881069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
882119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
882121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 
882154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
882222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
882242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
882247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
882254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
882257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
882258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
882260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
882263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
882266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
882268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
882270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
882458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
882460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
882461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
882462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
882463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
882601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
882603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
882604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
882606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
882607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
882608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
882777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
882779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
882780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
882781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
882782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
882783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
882906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
882908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
882909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
882909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
882910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
882911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
882918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
882919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
882920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
882922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
882923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
882924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
882931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
882932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
882933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
882934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
882935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
882936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
883076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
883077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
883079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
883216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
883218     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)'' 
883221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
883222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
883223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
883224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
883225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
883226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
883230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
883231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
883233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
883234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
883235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
883354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
883364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
883366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
883371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
883372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
883373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
883374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
883527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
883529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
883530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
883531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
883532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
883533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
883534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
883535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
883648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
883650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
883752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
883757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
883762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
883765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
883766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
883767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
883768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
883768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
883769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
883771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
883779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
883784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
883905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
883907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
883908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
883909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
883910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
883911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
883911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
883913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
883980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
883987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
884115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
884118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
884120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
884121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
884122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
884123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
884276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
884281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
884282     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)'' 
884284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
884286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
884287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
884288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
884289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
884298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
884300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
884301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
884303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
884415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
884416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
884417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
884418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
884419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
884420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
884544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
884546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
884547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
884549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
884550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
884551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
884551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
884553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
884655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
884657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
884751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
884751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
884752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
884758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
884763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
884769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
884918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
884920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
884921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
884922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
884936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
885082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
889785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
889787     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)'' 
889792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
889793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
889794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
889795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
889796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
889805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
889806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
889807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
889808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
889809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
889922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
889927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
889928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
889929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
889929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
889930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
889931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
890049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
890051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
890052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
890053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
890054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
890055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
890055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
890057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
890228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
890230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
890346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
890351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
890357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
890358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
890358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
890360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
890373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
890482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
890484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
890484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
890485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
890583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
890596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
890597     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)'' 
890600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
890601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
890602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
890603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
890603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
890617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
890618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
890619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
890620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
890621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
890729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
890731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
890732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
890733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
890734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
890853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
890859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
890861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
890865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
890866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
890867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
890868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
890988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
890991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
890992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
890994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
890995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
890998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
891000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
891001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
891002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
891003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
891004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
891005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
891005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
891005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
891006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
891120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
891122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
891130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
891232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
891335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
891337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
891338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
891339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
891340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
891340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
891341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
891341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
891343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
891446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
891453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
891561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
891562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
891563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
891564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
891564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
891565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
891565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
891566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
891573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
891573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
891675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
891681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
891688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
891815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
891817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
891817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
891819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
891819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
891819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
891820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
891821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
891891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
891893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
891893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
891894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
891895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
891902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
891909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
892051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
892216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
892217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
892218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
892220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
892424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
892534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
892535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
896278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
896284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
896286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
896286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
896287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
896441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
896443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
896444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
896444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
896445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
896570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
900355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
904237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
904243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
904244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
904245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
904246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
904445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
904447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
904448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
904449     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)' ...' 
904451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
905799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
905799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.1ns 
905800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
909148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
909148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
910254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
910256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
910257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
910264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
910277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
910280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
910282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
910283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
910288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
910290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
910293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
910296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
910296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
910307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
910309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
910310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
910365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
910366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
910367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
910368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
910369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
910441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
910442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
910444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
910445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
910445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
910449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
910450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
910450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
910452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
910453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
910453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
910546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
910548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
910548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
910550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
910551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
910551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
910653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
910654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
910655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
910655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
910656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
910657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
910658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
910658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
910659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
910660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
910660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
910661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
910662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
910662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
910663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
910664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
910665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
910666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
910667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
910669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
910713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
910715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
910774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
910775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
910777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
910778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
910779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
910780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
910828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
910831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
910833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
910834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
910835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
910836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
910837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
910896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
910899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
910903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
910966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
911033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
911034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
911035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
914401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
914401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
915521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
915576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.33ms