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

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
198
tests
failures
ignored
11m15.83s
duration
100%
successful
Tests
Standard output
Tests

Test	Method name	Duration	Result
powPositive	data()[100]	3.280s	passed
powPositiveConcrete	data()[101]	3.273s	passed
powGeq1Concrete	data()[102]	3.275s	passed
pow2InIntLower	data()[103]	3.281s	passed
pow2InIntUpper	data()[104]	3.300s	passed
logSelfConcrete	data()[105]	3.278s	passed
log1Concrete	data()[106]	3.275s	passed
logProduct	data()[107]	3.275s	passed
logTimesBaseConcrete	data()[108]	3.278s	passed
logProdIdentity	data()[109]	3.281s	passed
moduloByteIsInByte	data()[10]	3.402s	passed
logProdIdentityConcrete	data()[110]	3.272s	passed
logPowIdentity	data()[111]	3.272s	passed
logPowIdentityConcrete	data()[112]	3.268s	passed
logPositive	data()[113]	3.292s	passed
logPositiveConcrete	data()[114]	3.271s	passed
logMono	data()[115]	3.282s	passed
logMonoConcrete	data()[116]	3.287s	passed
powLogLess	data()[117]	3.284s	passed
powLogMore2	data()[118]	3.287s	passed
logLessThanPow	data()[119]	3.294s	passed
moduloCharIsInChar	data()[11]	3.373s	passed
logLessThanPowConcrete	data()[120]	3.279s	passed
logSqueeze	data()[121]	3.276s	passed
ifthenelse_equals	data()[122]	3.288s	passed
ifthenelse_equals_1	data()[123]	3.285s	passed
ifthenelse_equals_2	data()[124]	3.278s	passed
disjointWithSingleton1	data()[125]	3.319s	passed
disjointWithSingleton2	data()[126]	3.271s	passed
disjointArrayRanges	data()[127]	3.286s	passed
disjointArrayRangeAllFields1	data()[128]	3.301s	passed
disjointArrayRangeAllFields2	data()[129]	3.282s	passed
div_unique1	data()[12]	3.381s	passed
seqSelfDefinition	data()[130]	3.284s	passed
seqOutsideValue	data()[131]	3.320s	passed
castedGetAny	data()[132]	3.288s	passed
seqGetAlphaCast	data()[133]	3.290s	passed
getOfSeqSingleton	data()[134]	3.291s	passed
getOfSeqSingletonConcrete	data()[135]	3.290s	passed
getOfSeqConcat	data()[136]	3.319s	passed
getOfSeqSub	data()[137]	3.322s	passed
getOfSeqReverse	data()[138]	3.289s	passed
lenOfSeqEmpty	data()[139]	3.280s	passed
div_unique2	data()[13]	3.372s	passed
lenOfSeqSingleton	data()[140]	3.304s	passed
lenOfSeqConcat	data()[141]	3.288s	passed
lenOfSeqSub	data()[142]	3.286s	passed
lenOfSeqReverse	data()[143]	3.282s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.307s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.287s	passed
getOfSeqSingletonEQ	data()[146]	3.286s	passed
getOfSeqConcatEQ	data()[147]	3.299s	passed
getOfSeqSubEQ	data()[148]	3.276s	passed
getOfSeqReverseEQ	data()[149]	3.280s	passed
div_exists	data()[14]	3.454s	passed
lenOfSeqEmptyEQ	data()[150]	3.302s	passed
lenOfSeqSingletonEQ	data()[151]	3.284s	passed
lenOfSeqConcatEQ	data()[152]	3.306s	passed
lenOfSeqSubEQ	data()[153]	3.285s	passed
lenOfSeqReverseEQ	data()[154]	3.276s	passed
getOfSeqDefEQ	data()[155]	3.302s	passed
lenOfSeqDefEQ	data()[156]	3.279s	passed
seqConcatWithSeqEmpty1	data()[157]	3.313s	passed
seqConcatWithSeqEmpty2	data()[158]	3.302s	passed
seqReverseOfSeqEmpty	data()[159]	3.307s	passed
div_one	data()[15]	3.363s	passed
subSeqComplete	data()[160]	3.300s	passed
subSeqTailR	data()[161]	3.304s	passed
subSeqTailL	data()[162]	3.289s	passed
subSeqTailEQR	data()[163]	3.305s	passed
subSeqTailEQL	data()[164]	3.297s	passed
seqDef_split	data()[165]	3.322s	passed
seqDef_induction_upper	data()[166]	3.308s	passed
seqDef_induction_upper_concrete	data()[167]	3.316s	passed
seqDef_induction_lower	data()[168]	3.294s	passed
seqDef_induction_lower_concrete	data()[169]	3.316s	passed
jdiv_one	data()[16]	3.325s	passed
seqDef_split_in_three	data()[170]	3.360s	passed
seqDef_empty	data()[171]	3.286s	passed
seqDef_one_summand	data()[172]	3.313s	passed
seqDef_lower_equals_upper	data()[173]	3.278s	passed
seqDefOfSeq	data()[174]	3.312s	passed
seqSelfDefinitionEQ2	data()[175]	3.307s	passed
indexOfSeqSingleton	data()[176]	3.292s	passed
indexOfSeqConcatFirst	data()[177]	3.308s	passed
indexOfSeqConcatSecond	data()[178]	3.311s	passed
indexOfSeqSub	data()[179]	3.300s	passed
div_zero	data()[17]	3.375s	passed
lenOfArray2seq	data()[180]	3.303s	passed
getAnyOfArray2seq	data()[181]	3.295s	passed
getOfArray2seq	data()[182]	3.294s	passed
getAnyOfNPermInv	data()[183]	3.304s	passed
seqNPermRange	data()[184]	3.338s	passed
seqPermTrans	data()[185]	3.322s	passed
seqPermRefl	data()[186]	3.283s	passed
seqPermSplit	data()[187]	3.292s	passed
seqNPermRight	data()[188]	3.399s	passed
seqPermFromSwap	data()[189]	3.344s	passed
divResZero1	data()[18]	3.368s	passed
seqPermTransAlt0	data()[190]	3.310s	passed
seqPermTransAlt1	data()[191]	3.309s	passed
seqPermTransAlt2	data()[192]	3.280s	passed
seqPermTransAlt3	data()[193]	3.300s	passed
seqPermForall	data()[194]	3.395s	passed
seqPermExists	data()[195]	3.366s	passed
schiffl_lemma_2	data()[196]	21.404s	passed
schiffl_thm_1	data()[197]	4.086s	passed
eqSameSeq	data()[198]	3.435s	passed
divResZero2	data()[19]	3.365s	passed
eqTermCut	data()[1]	3.828s	passed
divResOne1	data()[20]	3.347s	passed
divResOne2	data()[21]	3.395s	passed
div_cancel1	data()[22]	3.441s	passed
div_cancel2	data()[23]	3.369s	passed
divAddMultDenom	data()[24]	3.408s	passed
divMinus	data()[25]	3.381s	passed
divMinusDenom	data()[26]	3.371s	passed
divLeastDPos	data()[27]	3.323s	passed
divLeastDNeg	data()[28]	3.319s	passed
divGreatestDPos	data()[29]	3.352s	passed
equivAllRight	data()[2]	3.617s	passed
divGreatestDNeg	data()[30]	3.312s	passed
divIncreasingPos	data()[31]	3.311s	passed
divIncreasingNeg	data()[32]	3.341s	passed
jdiv_zero	data()[33]	3.329s	passed
jdivPulloutMinusNum	data()[34]	3.306s	passed
jdivPulloutMinusDenom	data()[35]	3.339s	passed
jdiv_uniquePosPos	data()[36]	3.344s	passed
jdiv_uniquePosNeg	data()[37]	3.339s	passed
jdiv_uniqueNegPos	data()[38]	3.304s	passed
jdiv_uniqueNegNeg	data()[39]	3.309s	passed
irrflConcrete1	data()[3]	3.574s	passed
jdivMultDenom1	data()[40]	3.341s	passed
jdivMultDenom2	data()[41]	3.292s	passed
mod_geZero	data()[42]	3.312s	passed
mod_lessDenom	data()[43]	3.296s	passed
jmod_NumPos	data()[44]	3.299s	passed
jmod_NumNeg	data()[45]	3.301s	passed
jmod_geZero	data()[46]	3.303s	passed
jmodNumZero	data()[47]	3.358s	passed
jmod_pulloutminusNum	data()[48]	3.302s	passed
jmod_pulloutminusDenom	data()[49]	3.308s	passed
irrflConcrete2	data()[4]	3.572s	passed
jmodUnique1	data()[50]	3.347s	passed
jmodUnique2	data()[51]	3.359s	passed
intDivRem	data()[52]	3.290s	passed
jmodjmod	data()[53]	3.322s	passed
jmodDivisible	data()[54]	3.308s	passed
jmodDivisibleRep	data()[55]	3.291s	passed
jdivAddMultDenom	data()[56]	3.431s	passed
jmodAltZero	data()[57]	3.308s	passed
jmodAddMultDenomZero	data()[58]	3.289s	passed
polyDiv_zero	data()[59]	3.301s	passed
cancel_gtPos	data()[5]	3.443s	passed
polyMod_ltdivDenom	data()[60]	3.287s	passed
bsum_empty	data()[61]	3.268s	passed
bsum_induction_upper	data()[62]	3.276s	passed
bsum_induction_lower	data()[63]	3.293s	passed
bsum_num_of_bounds	data()[64]	3.290s	passed
bsum_num_of_bounds2	data()[65]	3.288s	passed
bsum_induction_upper2	data()[66]	3.273s	passed
bsum_induction_upper_concrete	data()[67]	3.284s	passed
bsum_induction_upper_concrete_2	data()[68]	3.285s	passed
bsum_induction_upper2_concrete	data()[69]	3.279s	passed
cancel_gtNeg	data()[6]	3.410s	passed
bsum_induction_lower_concrete	data()[70]	3.276s	passed
bsum_induction_lower2	data()[71]	3.302s	passed
bsum_induction_lower2_concrete	data()[72]	3.291s	passed
bsum_positive	data()[73]	3.319s	passed
bsum_upper_bound	data()[74]	3.307s	passed
bsum_lower_bound	data()[75]	3.295s	passed
bsum_positive_lower_bound_element	data()[76]	3.307s	passed
bsum_sub_same_index	data()[77]	3.306s	passed
bsum_less_same_index	data()[78]	3.309s	passed
bsum_equal_except_one_index	data()[79]	3.313s	passed
moduloIntIsInInt	data()[7]	3.385s	passed
bsum_num_of_is_max	data()[80]	3.285s	passed
bsum_num_of_is_max2	data()[81]	3.289s	passed
bsum_num_of_is_max3	data()[82]	3.326s	passed
bsum_num_of_is_max4	data()[83]	3.290s	passed
bsum_num_of_lt_max	data()[84]	3.317s	passed
bsum_num_of_lt_max2	data()[85]	3.300s	passed
bsum_num_of_lt_max3	data()[86]	3.299s	passed
bsum_num_of_lt_max4	data()[87]	3.304s	passed
bsum_num_of_gt0	data()[88]	3.298s	passed
bsum_num_of_gt0_alt	data()[89]	3.300s	passed
moduloLongIsInLong	data()[8]	3.363s	passed
bsum_add_concrete	data()[90]	3.281s	passed
bprod_all_positive	data()[91]	3.280s	passed
bprod_split	data()[92]	3.274s	passed
powConcrete0	data()[93]	3.293s	passed
powConcrete1	data()[94]	3.290s	passed
powSplitFactor	data()[95]	3.289s	passed
powAdd	data()[96]	3.286s	passed
powMono	data()[97]	3.280s	passed
powMonoConcrete	data()[98]	3.277s	passed
powMonoConcreteRight	data()[99]	3.292s	passed
moduloShortIsInShort	data()[9]	3.390s	passed
Standard output

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

1618       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1620       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1622       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1622       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3250       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8835       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.03s 
8896       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8929       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35ns 
8940       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8940       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.1ns 
8944       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11787      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
11789      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12738      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12762      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.72ms 
12771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355ns 
12773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15456      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
15461      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16374      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16386      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.85ms 
16390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16390      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.6ns 
16392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19111      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
19111      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19960      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
19962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19962      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149ns 
19963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22660      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
22661      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23532      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
23534      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23534      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.9ns 
23537      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26105      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
26106      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26938      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26975      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.89ms 
26977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.8ns 
26978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29530      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
29531      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30367      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30384      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.06ms 
30390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30390      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358ns 
30391      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32938      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
32938      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33773      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 726.8ns 
33775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33775      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313ns 
33776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36301      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
36301      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37135      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.4ns 
37138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.4ns 
37139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
39676      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40526      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.3ns 
40528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40528      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.7ns 
40529      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43081      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
43082      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43922      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43928      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
43931      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43931      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.2ns 
43933      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46471      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
46472      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
47299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
47302      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.2ns 
47304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
47304      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.3ns 
47306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49847      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
49847      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
50647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50683      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.53ms 
50686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50687      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.1ns 
50688      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53212      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
53212      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
54010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
54055      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.89ms 
54057      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
54058      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.5ns 
54060      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56593      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
56594      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
57393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
57509      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.29ms 
57512      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
57512      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140ns 
57513      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60051      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
60051      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
60869      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
60873      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
60875      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
60875      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.4ns 
60876      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63375      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
63376      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
64195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
64198      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
64200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
64200      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
64201      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66706      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
66706      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
67534      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
67572      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.44ms 
67575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
67575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.3ns 
67577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70101      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
70101      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
70929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
70941      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.76ms 
70943      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
70943      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.6ns 
70944      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
73449      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
74289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
74305      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.01ms 
74308      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
74310      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.17ms 
74314      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76817      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
76818      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
77640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
77653      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
77655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
77656      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352ns 
77657      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80200      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
80200      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
81036      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
81048      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.74ms 
81049      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
81050      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.7ns 
81051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83647      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
83647      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
84473      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
84489      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.82ms 
84490      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
84490      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.7ns 
84491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
87018      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
87854      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
87858      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
87859      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
87859      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns 
87860      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
90434      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
91230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
91266      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.51ms 
91269      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
91269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.9ns 
91270      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93803      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
93804      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
94602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
94646      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.11ms 
94649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
94650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.7ns 
94651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97169      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
97169      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
97988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
98019      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.39ms 
98023      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
98025      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.59ms 
98027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
100519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
101335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
101342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
101345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
101345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.3ns 
101346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
103835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
104650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
104662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.68ms 
104663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
104663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
104664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
107189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
108004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
108013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.52ms 
108015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
108015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
108016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
110498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
111318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
111325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.36ms 
111327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
111327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.1ns 
111327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
113811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
114629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
114636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
114638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
114639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.6ns 
114640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
117150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
117970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
117977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
117980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
117980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.4ns 
117981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
120476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
121301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
121306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
121308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
121308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.1ns 
121309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
123813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
124602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
124612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.13ms 
124614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
124614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.9ns 
124615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
127120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
127916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
127951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.93ms 
127953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
127954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307ns 
127955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
130471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
131263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
131294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.84ms 
131298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
131298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.2ns 
131300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
133802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
134618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
134634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.66ms 
134636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
134636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.7ns 
134637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
137113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
137924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
137939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.95ms 
137940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
137940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
137941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
140422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
141233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
141247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
141249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
141249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.9ns 
141250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
143746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
144556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
144588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.72ms 
144589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
144589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
144590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
147061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
147875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
147881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
147882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
147882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
147883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
150378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
151188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
151192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
151193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
151194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
151194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
153660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
154481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
154489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.33ms 
154490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
154490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
154491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
156965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
157780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
157787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
157789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
157789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
157790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
160284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
161071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
161088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.88ms 
161089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
161089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
161090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
163596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
164384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
164391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
164392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
164393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
164393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
166942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
167744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
167749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
167752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
167752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.8ns 
167756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
170259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
171047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
171051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
171053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
171054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.4ns 
171054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
173545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
174355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
174359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
174361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
174361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.6ns 
174362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
176842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
177651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
177706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.29ms 
177708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
177708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
177709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
180187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
181000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
181065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.88ms 
181068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
181068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.6ns 
181069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
183543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
184352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
184355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
184356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
184357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
184357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
186818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
187629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
187676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.31ms 
187679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
187684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.93ms 
187686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
190153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
190965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
190985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.17ms 
190986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
190986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
190987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
193453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
194264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
194269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
194285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
194287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.76ms 
194288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
196824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
197609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
197713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.7ms 
197714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
197714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
197715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
200213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
201008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
201022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.46ms 
201023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
201023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
201025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
203517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
204304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
204310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
204311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
204312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
204312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
206791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
207597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
207612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.82ms 
207613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
207613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
207614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
210081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
210888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
210897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.08ms 
210900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
210900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
210900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
213356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
214163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
214167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
214168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
214168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
214169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
216628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
217438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
217442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
217443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
217443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
217444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
219910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
220721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
220735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.86ms 
220737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
220737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
220738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
223204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
224013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
224025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.24ms 
224027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
224027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
224028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
226492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
227301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
227313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.71ms 
227314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
227314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
227315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
229775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
230584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
230587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 988.71ns 
230588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
230588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
230589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
233074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
233867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
233870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
233872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
233872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.4ns 
233873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
236363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
237151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
237155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
237157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
237157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
237157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
239646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
240432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
240434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.6ns 
240435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
240435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
240436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
242922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
243708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
243710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 520.6ns 
243711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
243712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
243712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
246200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
247009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
247012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
247014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
247014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
247014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
249488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
250301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
250303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.5ns 
250304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
250304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
250305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
252778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
253588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
253622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.08ms 
253623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
253623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
253624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
256091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
256900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
256929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.97ms 
256931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
256931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
256932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
259394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
260203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
260225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.05ms 
260226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
260226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
260227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
262688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
263500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
263530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.4ms 
263533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
263533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211ns 
263534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
266009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
266820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
266838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.95ms 
266839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
266840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
266840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
269307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
270113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
270147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.4ms 
270148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
270148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
270149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
272638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
273440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
273460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.8ms 
273462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
273462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.5ns 
273463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
275946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
276732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
276745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.61ms 
276747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
276747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
276747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
279234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
280019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
280035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.78ms 
280036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
280036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
280037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
282535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
283346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
283360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.28ms 
283367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
283367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
283368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
285831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
286639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
286655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.67ms 
286657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
286657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
286658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
289149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
289957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
289973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.77ms 
289974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
289974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
289975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
292438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
293255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
293272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.37ms 
293273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
293273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
293274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
295745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
296556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
296571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.26ms 
296572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
296573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
296573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
299050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
299861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
299875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.25ms 
299877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
299877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
299877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
302347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
303159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
303173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ms 
303175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
303175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
303175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
305650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
306459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
306473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.06ms 
306475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
306475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
306476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
308965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
309749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
309755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
309756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
309756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
309757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
312237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
313024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
313035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.28ms 
313036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
313036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
313037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
315519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
316305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
316308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
316310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
316310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
316310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
318789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
319599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
319601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.3ns 
319602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
319602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
319603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
322075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
322890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
322892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.3ns 
322893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
322893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
322894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
325357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
326168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
326180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.29ms 
326183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
326183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
326184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
328650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
329462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
329467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
329469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
329469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
329469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
331928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
332738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
332747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.08ms 
332748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
332749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
332749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
335212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
336021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
336024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
336026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
336026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
336027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
338499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
339314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
339316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 427ns 
339318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
339318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
339318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
341784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
342592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
342597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
342598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
342598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
342598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
345083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
345868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
345869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 493.8ns 
345871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
345871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
345871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
348357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
349143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
349145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 500.2ns 
349146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
349146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
349147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
351635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
352423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
352425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 497.7ns 
352426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
352426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
352427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
354908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
355695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
355726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.38ms 
355728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
355728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289ns 
355729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
358187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
358996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
359003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
359004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
359004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
359005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
361464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
362275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
362279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
362280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
362280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
362281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
364741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
365549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
365554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.29ms 
365555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
365555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
365556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
368019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
368828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
368832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
368833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
368833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
368834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
371291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
372101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
372113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.86ms 
372114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
372114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
372115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
374571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
375382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
375385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
375386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
375386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
375387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
377844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
378653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
378656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 990.3ns 
378657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
378657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
378658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
381113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
381921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
381924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
381925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
381925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
381926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
384411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
385203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
385216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.63ms 
385218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
385218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.8ns 
385219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
387697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
388482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
388487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 345.9ns 
388488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
388489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
388489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
390958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
391744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
391770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.44ms 
391771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
391771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
391772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
394246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
395054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
395057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
395058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
395058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
395059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
397518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
398326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
398340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.81ms 
398342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
398342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
398342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
400804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
401614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
401627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.21ms 
401629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
401629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
401629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
404095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
404904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
404921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.28ms 
404923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
404923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
404924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
407389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
408199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
408201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 489ns 
408202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
408202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
408203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
410662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
411472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
411477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
411478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
411478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
411479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
413947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
414762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
414765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
414766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
414766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
414767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
417256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
418047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
418049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.2ns 
418051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
418051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
418052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
420533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
421325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
421327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.3ns 
421328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
421328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
421329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
423819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
424615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
424646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.91ms 
424647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
424648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
424648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
427103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
427915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
427918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 992.3ns 
427919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
427919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
427920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
430381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
431195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
431203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
431205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
431205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.4ns 
431206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
433679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
434498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
434504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
434505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
434505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
434506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
436966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
437781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
437786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
437788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
437788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
437788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
440266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
441064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
441071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
441072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
441072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
441073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
443551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
444387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
444391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
444392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
444392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
444393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
446851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
447675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
447679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
447680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
447680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
447681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
450142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
450965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
450968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 679.8ns 
450970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
450970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.6ns 
450971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
453433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
454256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
454259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 869ns 
454261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
454261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.2ns 
454262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
456746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
457547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
457549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.7ns 
457550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
457550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
457551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
460037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
460860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
460868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.08ms 
460869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
460869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
460870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
463365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
464187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
464190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
464191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
464191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
464192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
466653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
467475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
467480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
467481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
467481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
467482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
469959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
470757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
470760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 727.7ns 
470761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
470761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
470761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
473238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
474061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
474063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 543.6ns 
474065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
474065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
474065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
476526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
477349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
477351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
477353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
477353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
477354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
479814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
480635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
480638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.4ns 
480639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
480639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
480640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
483117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
483917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
483919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.41ns 
483920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
483921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
483921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
486398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
487224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
487227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 852.21ns 
487228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
487228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
487229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
489687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
490510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
490513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
490514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
490515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
490515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
492998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
493797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
493800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 769.61ns 
493801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
493801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
493802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
496270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
497091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
497099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 
497100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
497100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
497101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
499551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
500372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
500374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 472.3ns 
500375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
500376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
500376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
502850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
503649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
503654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
503656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
503656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
503656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
506132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
506954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
506956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 743.31ns 
506958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
506958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.7ns 
506959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
509418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
510238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
510240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 604.01ns 
510241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
510241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
510242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
512720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
513541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
513546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
513548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
513548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.1ns 
513549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
516009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
516829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
516831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 922.3ns 
516833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
516833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
516833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
519305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
520104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
520107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
520108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
520108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
520109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
522585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
523407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
523409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
523411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
523411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
523411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
525862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
526685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
526688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
526690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
526690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
526690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
529170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
529992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
530001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 
530003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
530003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
530004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
532475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
533296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
533303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
533305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
533305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
533305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
535784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
536605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
536611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
536612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
536612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
536613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
539081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
539905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
539910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
539912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
539912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
539912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
542386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
543205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
543214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
543216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
543216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
543216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
545672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
546494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
546504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.44ms 
546505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
546505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
546506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
548980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
549799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
549809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.07ms 
549810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
549810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
549811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
552273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
553099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
553106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
553107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
553107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
553108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
555587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
556409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
556428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.75ms 
556429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
556429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
556430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
558891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
559714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
559735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.01ms 
559736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
559737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
559737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
562211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
563032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
563051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.45ms 
563052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
563053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
563053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
565507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
566327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
566345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.78ms 
566347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
566347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
566347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
568821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
569643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
569661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.65ms 
569663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
569663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
569664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
572143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
572944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
573021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.6ms 
573022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
573023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
573023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
575479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
576302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
576307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
576308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
576308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
576309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
578793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
579616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
579620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
579621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
579622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
579622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
582073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
582895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
582898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
582899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
582899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
582900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
585374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
586198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
586210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.63ms 
586211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
586212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
586212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
588689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
589511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
589517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.08ms 
589518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
589518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
589519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
591982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
592807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
592810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
592811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
592811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
592812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
595287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
596108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
596117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
596118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
596119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
596119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
598595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
599418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
599428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.86ms 
599430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
599430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
599430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
601891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
602715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
602728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.26ms 
602730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
602730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.2ns 
602731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
605207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
606029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
606031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 945.4ns 
606032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
606032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
606033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
608502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
609323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
609326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
609328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
609328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
609328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
611805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
612615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
612620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
612622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
612622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
612622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
615100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
615920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
615925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
615926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
615926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
615927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
618399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
619220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
619262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.99ms 
619264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
619264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
619265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
621739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
622563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
622584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.89ms 
622586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
622586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
622586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
625057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
625856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
625867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.77ms 
625868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
625868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
625869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
628336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
629158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
629160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 152.8ns 
629161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
629161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
629162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
631652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
632476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
632558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.53ms 
632559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
632559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
632560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
635041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
635869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
635902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.93ms 
635904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
635904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
635904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
638385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
639210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
639212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 261.1ns 
639214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
639214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
639214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
641698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
642520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
642522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 214.3ns 
642523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
642523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
642524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
644999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
645800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
645802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 202ns 
645803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
645803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
645804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
648276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
649099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
649101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.2ns 
649102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
649102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
649103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
651569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
652392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
652496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.02ms 
652498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
652498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.9ns 
652499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
654987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
655815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
655862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.24ms 
655864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
655864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
655865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
658343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
659168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
659170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
659199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 49) 
659245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' on goal 3 (script from line 50) 
659263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' on goal 4 (script from line 51) 
659269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' on goal 5 (script from line 52) 
659282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' on goal 11 (script from line 53) 
659283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' on goal 12 (script from line 54) 
659285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' on goal 13 (script from line 55) 
659286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 14 (script from line 56) 
659291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' on goal 16 (script from line 58) 
659294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' on goal 17 (script from line 59) 
659296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' on goal 18 (script from line 60) 
659299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' on goal 19 (script from line 61) 
659534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' on goal 20 (script from line 62) 
659535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' on goal 97 (script from line 63) 
659536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' on goal 98 (script from line 65) 
659537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' on goal 99 (script from line 66) 
659538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' on goal 100 (script from line 67) 
659645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' on goal 101 (script from line 68) 
659646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' on goal 188 (script from line 69) 
659647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' on goal 189 (script from line 71) 
659648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' on goal 190 (script from line 72) 
659650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' on goal 191 (script from line 73) 
659651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' on goal 192 (script from line 74) 
659801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' on goal 193 (script from line 75) 
659802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 310 (script from line 76) 
659803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 311 (script from line 77) 
659804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' on goal 312 (script from line 79) 
659805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' on goal 313 (script from line 80) 
659806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' on goal 314 (script from line 81) 
659919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' on goal 315 (script from line 82) 
659920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 420 (script from line 83) 
659921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 421 (script from line 84) 
659922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' on goal 422 (script from line 86) 
659923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' on goal 423 (script from line 87) 
659924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' on goal 424 (script from line 88) 
659930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' on goal 425 (script from line 89) 
659931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 434 (script from line 90) 
659933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' on goal 435 (script from line 91) 
659934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' on goal 436 (script from line 93) 
659934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' on goal 437 (script from line 94) 
659935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' on goal 438 (script from line 95) 
659942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' on goal 439 (script from line 96) 
659943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' on goal 448 (script from line 97) 
659944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' on goal 449 (script from line 98) 
659945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' on goal 450 (script from line 100) 
659945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' on goal 451 (script from line 101) 
659946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' on goal 452 (script from line 102) 
660066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' on goal 453 (script from line 104) 
660067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' on goal 562 (script from line 105) 
660068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' on goal 563 (script from line 106) 
660172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' on goal 564 (script from line 108) 
660173     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)'' on goal 674 (script from line 110) 
660175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' on goal 676 (script from line 112) 
660177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' on goal 677 (script from line 113) 
660178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' on goal 679 (script from line 114) 
660179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' on goal 681 (script from line 115) 
660179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' on goal 683 (script from line 116) 
660180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 685 (script from line 117) 
660186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' on goal 684 (script from line 119) 
660187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' on goal 687 (script from line 120) 
660188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' on goal 688 (script from line 121) 
660189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' on goal 689 (script from line 122) 
660190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' on goal 690 (script from line 123) 
660284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 691 (script from line 124) 
660288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' on goal 682 (script from line 126) 
660289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' on goal 796 (script from line 127) 
660290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' on goal 797 (script from line 128) 
660291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' on goal 798 (script from line 129) 
660292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' on goal 799 (script from line 130) 
660293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' on goal 800 (script from line 131) 
660403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' on goal 801 (script from line 132) 
660404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' on goal 912 (script from line 133) 
660405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' on goal 913 (script from line 134) 
660407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' on goal 914 (script from line 135) 
660408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' on goal 916 (script from line 136) 
660408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' on goal 917 (script from line 137) 
660409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' on goal 918 (script from line 138) 
660410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' on goal 919 (script from line 139) 
660496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' on goal 920 (script from line 140) 
660497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' on goal 1011 (script from line 141) 
660583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' on goal 1012 (script from line 142) 
660588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' on goal 915 (script from line 143) 
660592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' on goal 680 (script from line 145) 
660593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' on goal 1099 (script from line 146) 
660594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' on goal 1100 (script from line 147) 
660595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' on goal 1101 (script from line 148) 
660596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' on goal 1103 (script from line 149) 
660596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' on goal 1104 (script from line 150) 
660597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' on goal 1105 (script from line 151) 
660598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' on goal 1106 (script from line 152) 
660605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' on goal 1107 (script from line 153) 
660610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' on goal 1102 (script from line 154) 
660706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' on goal 678 (script from line 156) 
660707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' on goal 1225 (script from line 157) 
660708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' on goal 1226 (script from line 158) 
660709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' on goal 1227 (script from line 159) 
660710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' on goal 1229 (script from line 160) 
660710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' on goal 1230 (script from line 161) 
660711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' on goal 1231 (script from line 162) 
660711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' on goal 1232 (script from line 163) 
660764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' on goal 1233 (script from line 164) 
660770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' on goal 1228 (script from line 165) 
660902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' on goal 675 (script from line 168) 
660903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' on goal 1397 (script from line 169) 
660904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' on goal 1399 (script from line 170) 
660905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' on goal 1400 (script from line 171) 
660910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' on goal 1401 (script from line 172) 
660911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' on goal 1402 (script from line 173) 
661036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' on goal 1403 (script from line 174) 
661040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' on goal 1398 (script from line 176) 
661041     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)'' on goal 1534 (script from line 178) 
661041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' on goal 1536 (script from line 180) 
661043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' on goal 1537 (script from line 181) 
661044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' on goal 1539 (script from line 182) 
661045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' on goal 1541 (script from line 183) 
661045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' on goal 1543 (script from line 184) 
661055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' on goal 1544 (script from line 186) 
661056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' on goal 1558 (script from line 187) 
661057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' on goal 1559 (script from line 188) 
661058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' on goal 1560 (script from line 189) 
661152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' on goal 1542 (script from line 191) 
661153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' on goal 1667 (script from line 192) 
661154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' on goal 1668 (script from line 193) 
661155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' on goal 1669 (script from line 194) 
661155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' on goal 1670 (script from line 195) 
661156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' on goal 1671 (script from line 196) 
661252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' on goal 1672 (script from line 197) 
661253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' on goal 1786 (script from line 198) 
661255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' on goal 1787 (script from line 199) 
661256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' on goal 1788 (script from line 200) 
661256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' on goal 1790 (script from line 201) 
661257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' on goal 1791 (script from line 202) 
661258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' on goal 1792 (script from line 203) 
661258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' on goal 1793 (script from line 204) 
661342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' on goal 1794 (script from line 205) 
661344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' on goal 1885 (script from line 206) 
661426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' on goal 1886 (script from line 207) 
661427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' on goal 1968 (script from line 208) 
661428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' on goal 1969 (script from line 209) 
661433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' on goal 1970 (script from line 210) 
661437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' on goal 1789 (script from line 211) 
661441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' on goal 1540 (script from line 212) 
661572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' on goal 1538 (script from line 214) 
661573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' on goal 2097 (script from line 215) 
661574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' on goal 2098 (script from line 216) 
661575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' on goal 2099 (script from line 217) 
661585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' on goal 2100 (script from line 218) 
661677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' on goal 1535 (script from line 220) 
665022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' on goal 1535 (script from line 223) 
665023     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)'' on goal 4266 (script from line 225) 
665026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' on goal 4268 (script from line 227) 
665030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' on goal 4269 (script from line 228) 
665030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' on goal 4271 (script from line 229) 
665031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' on goal 4273 (script from line 230) 
665032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' on goal 4275 (script from line 231) 
665040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' on goal 4276 (script from line 233) 
665040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' on goal 4287 (script from line 234) 
665041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' on goal 4288 (script from line 235) 
665042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' on goal 4289 (script from line 236) 
665043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' on goal 4290 (script from line 237) 
665191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' on goal 4291 (script from line 238) 
665194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' on goal 4274 (script from line 240) 
665195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' on goal 4400 (script from line 241) 
665196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' on goal 4401 (script from line 242) 
665196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' on goal 4402 (script from line 243) 
665197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' on goal 4403 (script from line 244) 
665197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' on goal 4404 (script from line 245) 
665291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' on goal 4405 (script from line 246) 
665292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' on goal 4521 (script from line 247) 
665292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' on goal 4522 (script from line 248) 
665295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' on goal 4523 (script from line 249) 
665295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' on goal 4525 (script from line 250) 
665296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' on goal 4526 (script from line 251) 
665296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' on goal 4527 (script from line 252) 
665297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' on goal 4528 (script from line 253) 
665372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' on goal 4529 (script from line 254) 
665373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' on goal 4622 (script from line 255) 
665443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' on goal 4623 (script from line 256) 
665447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' on goal 4524 (script from line 257) 
665451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' on goal 4272 (script from line 259) 
665452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' on goal 4713 (script from line 260) 
665453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' on goal 4714 (script from line 261) 
665454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' on goal 4715 (script from line 262) 
665463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' on goal 4716 (script from line 263) 
665539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' on goal 4270 (script from line 265) 
665540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' on goal 4839 (script from line 266) 
665541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' on goal 4840 (script from line 267) 
665542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' on goal 4841 (script from line 268) 
665610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' on goal 4842 (script from line 269) 
665619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' on goal 4267 (script from line 272) 
665619     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)'' on goal 4948 (script from line 274) 
665620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' on goal 4950 (script from line 276) 
665621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' on goal 4951 (script from line 277) 
665621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' on goal 4953 (script from line 278) 
665622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' on goal 4955 (script from line 279) 
665622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' on goal 4957 (script from line 280) 
665633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' on goal 4958 (script from line 282) 
665633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' on goal 4977 (script from line 283) 
665634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' on goal 4978 (script from line 284) 
665635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' on goal 4979 (script from line 285) 
665635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' on goal 4980 (script from line 286) 
665718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' on goal 4981 (script from line 287) 
665719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' on goal 5093 (script from line 288) 
665720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' on goal 5094 (script from line 289) 
665720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' on goal 5095 (script from line 290) 
665721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' on goal 5096 (script from line 291) 
665807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' on goal 5097 (script from line 292) 
665811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' on goal 4956 (script from line 294) 
665812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' on goal 5212 (script from line 295) 
665813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' on goal 5213 (script from line 296) 
665813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' on goal 5214 (script from line 299) 
665814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' on goal 5215 (script from line 300) 
665814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' on goal 5216 (script from line 301) 
665908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' on goal 5217 (script from line 303) 
665909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' on goal 5337 (script from line 304) 
665910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' on goal 5338 (script from line 305) 
665911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' on goal 5339 (script from line 306) 
665911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' on goal 5341 (script from line 307) 
665912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' on goal 5342 (script from line 308) 
665914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' on goal 5343 (script from line 309) 
665915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' on goal 5344 (script from line 310) 
665915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' on goal 5346 (script from line 311) 
665916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' on goal 5347 (script from line 312) 
665917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' on goal 5348 (script from line 313) 
665917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' on goal 5350 (script from line 314) 
665918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' on goal 5351 (script from line 315) 
665918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' on goal 5352 (script from line 316) 
665919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' on goal 5353 (script from line 317) 
666002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' on goal 5354 (script from line 318) 
666003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' on goal 5463 (script from line 319) 
666009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' on goal 5464 (script from line 320) 
666083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' on goal 5349 (script from line 321) 
666160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' on goal 5345 (script from line 323) 
666161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' on goal 5660 (script from line 324) 
666162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' on goal 5662 (script from line 325) 
666162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' on goal 5663 (script from line 326) 
666163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' on goal 5664 (script from line 327) 
666164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' on goal 5666 (script from line 328) 
666164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' on goal 5667 (script from line 329) 
666164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' on goal 5668 (script from line 330) 
666165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' on goal 5669 (script from line 331) 
666247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' on goal 5670 (script from line 332) 
666253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' on goal 5665 (script from line 333) 
666339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' on goal 5661 (script from line 335) 
666340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' on goal 5887 (script from line 336) 
666341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' on goal 5888 (script from line 337) 
666342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' on goal 5889 (script from line 338) 
666342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' on goal 5891 (script from line 339) 
666343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' on goal 5892 (script from line 340) 
666343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' on goal 5893 (script from line 341) 
666344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' on goal 5894 (script from line 342) 
666349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' on goal 5895 (script from line 343) 
666350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' on goal 5897 (script from line 344) 
666426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' on goal 5898 (script from line 345) 
666432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' on goal 5890 (script from line 346) 
666438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' on goal 5340 (script from line 347) 
666533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' on goal 4954 (script from line 349) 
666534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' on goal 6115 (script from line 350) 
666535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' on goal 6116 (script from line 351) 
666536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' on goal 6117 (script from line 352) 
666537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' on goal 6119 (script from line 353) 
666537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' on goal 6120 (script from line 354) 
666538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' on goal 6121 (script from line 355) 
666539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' on goal 6122 (script from line 356) 
666592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' on goal 6123 (script from line 357) 
666593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' on goal 6193 (script from line 358) 
666594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' on goal 6195 (script from line 359) 
666594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' on goal 6196 (script from line 360) 
666595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' on goal 6197 (script from line 361) 
666601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' on goal 6198 (script from line 362) 
666607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' on goal 6194 (script from line 363) 
666719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' on goal 6118 (script from line 364) 
666804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' on goal 4952 (script from line 366) 
666805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' on goal 6456 (script from line 367) 
666805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' on goal 6457 (script from line 368) 
666806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' on goal 6458 (script from line 369) 
667013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' on goal 6459 (script from line 370) 
667096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' on goal 4949 (script from line 374) 
667097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' on goal 6735 (script from line 377) 
669951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' on goal 6735 (script from line 379) 
669955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' on goal 8783 (script from line 380) 
669955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' on goal 8784 (script from line 381) 
669956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' on goal 8785 (script from line 382) 
669957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' on goal 8786 (script from line 383) 
670065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' on goal 8787 (script from line 384) 
670066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' on goal 8909 (script from line 385) 
670067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' on goal 8910 (script from line 386) 
670067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' on goal 8911 (script from line 387) 
670068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' on goal 8912 (script from line 388) 
670168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' on goal 8913 (script from line 389) 
673031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' on goal 6736 (script from line 396) 
676080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' on goal 6736 (script from line 398) 
676083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' on goal 12633 (script from line 399) 
676084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' on goal 12634 (script from line 400) 
676085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' on goal 12635 (script from line 401) 
676086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' on goal 12636 (script from line 402) 
676195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' on goal 12637 (script from line 403) 
676195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' on goal 12757 (script from line 404) 
676196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' on goal 12758 (script from line 405) 
676197     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)' ...' on goal 12759 (script from line 406) 
676198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' on goal 12760 (script from line 407) 
677268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
677268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
677269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
679837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
680679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
680680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
680681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 50) 
680690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' on goal 10 (script from line 51) 
680698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' on goal 11 (script from line 52) 
680701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' on goal 12 (script from line 53) 
680703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' on goal 13 (script from line 54) 
680704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' on goal 14 (script from line 55) 
680709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' on goal 15 (script from line 56) 
680710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 23 (script from line 57) 
680714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' on goal 27 (script from line 58) 
680715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' on goal 28 (script from line 59) 
680717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' on goal 29 (script from line 60) 
680727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' on goal 30 (script from line 61) 
680727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' on goal 46 (script from line 62) 
680729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' on goal 47 (script from line 63) 
680780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' on goal 48 (script from line 64) 
680780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' on goal 119 (script from line 65) 
680781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' on goal 120 (script from line 66) 
680781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' on goal 121 (script from line 67) 
680782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' on goal 122 (script from line 68) 
680853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' on goal 123 (script from line 69) 
680853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' on goal 203 (script from line 70) 
680854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' on goal 204 (script from line 71) 
680855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' on goal 205 (script from line 72) 
680855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' on goal 206 (script from line 73) 
680859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 207 (script from line 74) 
680860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 215 (script from line 75) 
680860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' on goal 216 (script from line 76) 
680860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' on goal 217 (script from line 77) 
680861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' on goal 218 (script from line 78) 
680862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' on goal 219 (script from line 79) 
680948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 220 (script from line 80) 
680949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 311 (script from line 81) 
680949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' on goal 312 (script from line 82) 
680950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' on goal 313 (script from line 83) 
680951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' on goal 314 (script from line 84) 
680952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' on goal 315 (script from line 85) 
681039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 316 (script from line 86) 
681040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' on goal 410 (script from line 87) 
681040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' on goal 411 (script from line 88) 
681040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' on goal 412 (script from line 89) 
681041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' on goal 413 (script from line 90) 
681042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' on goal 414 (script from line 91) 
681042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' on goal 416 (script from line 92) 
681042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' on goal 417 (script from line 93) 
681043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' on goal 418 (script from line 94) 
681043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' on goal 420 (script from line 95) 
681044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' on goal 421 (script from line 96) 
681044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' on goal 422 (script from line 97) 
681044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' on goal 423 (script from line 98) 
681045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' on goal 424 (script from line 99) 
681045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' on goal 425 (script from line 100) 
681045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' on goal 426 (script from line 101) 
681046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' on goal 427 (script from line 102) 
681046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' on goal 428 (script from line 103) 
681047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' on goal 430 (script from line 104) 
681049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' on goal 431 (script from line 105) 
681084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' on goal 429 (script from line 106) 
681085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 473 (script from line 107) 
681139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' on goal 474 (script from line 108) 
681140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' on goal 541 (script from line 109) 
681140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' on goal 543 (script from line 110) 
681141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' on goal 544 (script from line 111) 
681142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' on goal 545 (script from line 112) 
681143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 546 (script from line 113) 
681190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' on goal 547 (script from line 114) 
681192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' on goal 542 (script from line 115) 
681193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' on goal 606 (script from line 116) 
681193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' on goal 608 (script from line 117) 
681194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' on goal 609 (script from line 118) 
681195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' on goal 610 (script from line 119) 
681196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' on goal 611 (script from line 120) 
681244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' on goal 612 (script from line 121) 
681247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' on goal 607 (script from line 122) 
681250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' on goal 419 (script from line 123) 
681300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' on goal 415 (script from line 124) 
681353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
681354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
681354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
683895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
684772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
684787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.27ms