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

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

Test	Method name	Duration	Result
powPositive	data()[100]	3.898s	passed
powPositiveConcrete	data()[101]	3.990s	passed
powGeq1Concrete	data()[102]	3.797s	passed
pow2InIntLower	data()[103]	3.847s	passed
pow2InIntUpper	data()[104]	3.812s	passed
logSelfConcrete	data()[105]	3.860s	passed
log1Concrete	data()[106]	3.856s	passed
logProduct	data()[107]	3.938s	passed
logTimesBaseConcrete	data()[108]	3.972s	passed
logProdIdentity	data()[109]	3.901s	passed
moduloByteIsInByte	data()[10]	4.178s	passed
logProdIdentityConcrete	data()[110]	3.894s	passed
logPowIdentity	data()[111]	3.847s	passed
logPowIdentityConcrete	data()[112]	3.912s	passed
logPositive	data()[113]	3.876s	passed
logPositiveConcrete	data()[114]	3.930s	passed
logMono	data()[115]	3.849s	passed
logMonoConcrete	data()[116]	3.794s	passed
powLogLess	data()[117]	3.858s	passed
powLogMore2	data()[118]	3.848s	passed
logLessThanPow	data()[119]	3.854s	passed
moduloCharIsInChar	data()[11]	4.002s	passed
logLessThanPowConcrete	data()[120]	3.851s	passed
logSqueeze	data()[121]	3.835s	passed
ifthenelse_equals	data()[122]	3.852s	passed
ifthenelse_equals_1	data()[123]	3.820s	passed
ifthenelse_equals_2	data()[124]	3.806s	passed
disjointWithSingleton1	data()[125]	3.904s	passed
disjointWithSingleton2	data()[126]	3.933s	passed
disjointArrayRanges	data()[127]	3.962s	passed
disjointArrayRangeAllFields1	data()[128]	4.110s	passed
disjointArrayRangeAllFields2	data()[129]	3.976s	passed
div_unique1	data()[12]	4.246s	passed
seqSelfDefinition	data()[130]	4.077s	passed
seqOutsideValue	data()[131]	3.855s	passed
castedGetAny	data()[132]	3.860s	passed
seqGetAlphaCast	data()[133]	3.822s	passed
getOfSeqSingleton	data()[134]	3.863s	passed
getOfSeqSingletonConcrete	data()[135]	3.820s	passed
getOfSeqConcat	data()[136]	4.097s	passed
getOfSeqSub	data()[137]	4.070s	passed
getOfSeqReverse	data()[138]	4.177s	passed
lenOfSeqEmpty	data()[139]	4.175s	passed
div_unique2	data()[13]	4.081s	passed
lenOfSeqSingleton	data()[140]	4.160s	passed
lenOfSeqConcat	data()[141]	4.106s	passed
lenOfSeqSub	data()[142]	4.199s	passed
lenOfSeqReverse	data()[143]	4.098s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	4.144s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	4.227s	passed
getOfSeqSingletonEQ	data()[146]	4.131s	passed
getOfSeqConcatEQ	data()[147]	4.162s	passed
getOfSeqSubEQ	data()[148]	4.157s	passed
getOfSeqReverseEQ	data()[149]	4.106s	passed
div_exists	data()[14]	4.197s	passed
lenOfSeqEmptyEQ	data()[150]	4.079s	passed
lenOfSeqSingletonEQ	data()[151]	4.026s	passed
lenOfSeqConcatEQ	data()[152]	4.121s	passed
lenOfSeqSubEQ	data()[153]	4.062s	passed
lenOfSeqReverseEQ	data()[154]	4.052s	passed
getOfSeqDefEQ	data()[155]	4.011s	passed
lenOfSeqDefEQ	data()[156]	3.999s	passed
seqConcatWithSeqEmpty1	data()[157]	4.032s	passed
seqConcatWithSeqEmpty2	data()[158]	4.045s	passed
seqReverseOfSeqEmpty	data()[159]	3.977s	passed
div_one	data()[15]	4.017s	passed
subSeqComplete	data()[160]	4.075s	passed
subSeqTailR	data()[161]	4.072s	passed
subSeqTailL	data()[162]	3.986s	passed
subSeqTailEQR	data()[163]	3.958s	passed
subSeqTailEQL	data()[164]	3.964s	passed
seqDef_split	data()[165]	4.010s	passed
seqDef_induction_upper	data()[166]	3.958s	passed
seqDef_induction_upper_concrete	data()[167]	3.914s	passed
seqDef_induction_lower	data()[168]	3.898s	passed
seqDef_induction_lower_concrete	data()[169]	3.948s	passed
jdiv_one	data()[16]	4.057s	passed
seqDef_split_in_three	data()[170]	3.921s	passed
seqDef_empty	data()[171]	3.816s	passed
seqDef_one_summand	data()[172]	3.873s	passed
seqDef_lower_equals_upper	data()[173]	3.814s	passed
seqDefOfSeq	data()[174]	3.824s	passed
seqSelfDefinitionEQ2	data()[175]	3.859s	passed
indexOfSeqSingleton	data()[176]	3.864s	passed
indexOfSeqConcatFirst	data()[177]	3.909s	passed
indexOfSeqConcatSecond	data()[178]	4.008s	passed
indexOfSeqSub	data()[179]	4.016s	passed
div_zero	data()[17]	4.030s	passed
lenOfArray2seq	data()[180]	4.056s	passed
getAnyOfArray2seq	data()[181]	3.853s	passed
getOfArray2seq	data()[182]	3.870s	passed
getAnyOfNPermInv	data()[183]	3.791s	passed
seqNPermRange	data()[184]	3.862s	passed
seqPermTrans	data()[185]	3.846s	passed
seqPermRefl	data()[186]	3.832s	passed
seqPermSplit	data()[187]	3.813s	passed
seqNPermRight	data()[188]	3.985s	passed
seqPermFromSwap	data()[189]	3.918s	passed
divResZero1	data()[18]	4.042s	passed
seqPermTransAlt0	data()[190]	3.831s	passed
seqPermTransAlt1	data()[191]	4.027s	passed
seqPermTransAlt2	data()[192]	3.949s	passed
seqPermTransAlt3	data()[193]	3.952s	passed
seqPermForall	data()[194]	4.206s	passed
seqPermExists	data()[195]	4.149s	passed
schiffl_lemma_2	data()[196]	28.756s	passed
schiffl_thm_1	data()[197]	4.748s	passed
eqSameSeq	data()[198]	4.049s	passed
divResZero2	data()[19]	4.013s	passed
eqTermCut	data()[1]	4.893s	passed
divResOne1	data()[20]	4.022s	passed
divResOne2	data()[21]	4.049s	passed
div_cancel1	data()[22]	4.059s	passed
div_cancel2	data()[23]	3.979s	passed
divAddMultDenom	data()[24]	4.008s	passed
divMinus	data()[25]	4.120s	passed
divMinusDenom	data()[26]	4.017s	passed
divLeastDPos	data()[27]	4.073s	passed
divLeastDNeg	data()[28]	4.028s	passed
divGreatestDPos	data()[29]	4.113s	passed
equivAllRight	data()[2]	4.605s	passed
divGreatestDNeg	data()[30]	4.150s	passed
divIncreasingPos	data()[31]	4.071s	passed
divIncreasingNeg	data()[32]	3.985s	passed
jdiv_zero	data()[33]	3.969s	passed
jdivPulloutMinusNum	data()[34]	4.006s	passed
jdivPulloutMinusDenom	data()[35]	4.059s	passed
jdiv_uniquePosPos	data()[36]	3.930s	passed
jdiv_uniquePosNeg	data()[37]	3.979s	passed
jdiv_uniqueNegPos	data()[38]	3.947s	passed
jdiv_uniqueNegNeg	data()[39]	3.928s	passed
irrflConcrete1	data()[3]	4.569s	passed
jdivMultDenom1	data()[40]	3.983s	passed
jdivMultDenom2	data()[41]	3.982s	passed
mod_geZero	data()[42]	3.983s	passed
mod_lessDenom	data()[43]	3.907s	passed
jmod_NumPos	data()[44]	3.910s	passed
jmod_NumNeg	data()[45]	3.978s	passed
jmod_geZero	data()[46]	3.955s	passed
jmodNumZero	data()[47]	3.946s	passed
jmod_pulloutminusNum	data()[48]	3.987s	passed
jmod_pulloutminusDenom	data()[49]	3.905s	passed
irrflConcrete2	data()[4]	4.304s	passed
jmodUnique1	data()[50]	4.140s	passed
jmodUnique2	data()[51]	4.149s	passed
intDivRem	data()[52]	3.958s	passed
jmodjmod	data()[53]	4.176s	passed
jmodDivisible	data()[54]	4.150s	passed
jmodDivisibleRep	data()[55]	4.161s	passed
jdivAddMultDenom	data()[56]	4.203s	passed
jmodAltZero	data()[57]	4.243s	passed
jmodAddMultDenomZero	data()[58]	4.123s	passed
polyDiv_zero	data()[59]	4.212s	passed
cancel_gtPos	data()[5]	4.115s	passed
polyMod_ltdivDenom	data()[60]	4.184s	passed
bsum_empty	data()[61]	4.105s	passed
bsum_induction_upper	data()[62]	4.113s	passed
bsum_induction_lower	data()[63]	4.070s	passed
bsum_num_of_bounds	data()[64]	4.180s	passed
bsum_num_of_bounds2	data()[65]	4.077s	passed
bsum_induction_upper2	data()[66]	3.953s	passed
bsum_induction_upper_concrete	data()[67]	3.939s	passed
bsum_induction_upper_concrete_2	data()[68]	3.915s	passed
bsum_induction_upper2_concrete	data()[69]	3.951s	passed
cancel_gtNeg	data()[6]	4.095s	passed
bsum_induction_lower_concrete	data()[70]	3.842s	passed
bsum_induction_lower2	data()[71]	3.835s	passed
bsum_induction_lower2_concrete	data()[72]	3.844s	passed
bsum_positive	data()[73]	4.018s	passed
bsum_upper_bound	data()[74]	4.024s	passed
bsum_lower_bound	data()[75]	3.964s	passed
bsum_positive_lower_bound_element	data()[76]	3.938s	passed
bsum_sub_same_index	data()[77]	3.877s	passed
bsum_less_same_index	data()[78]	4.106s	passed
bsum_equal_except_one_index	data()[79]	4.225s	passed
moduloIntIsInInt	data()[7]	4.012s	passed
bsum_num_of_is_max	data()[80]	4.041s	passed
bsum_num_of_is_max2	data()[81]	4.124s	passed
bsum_num_of_is_max3	data()[82]	4.059s	passed
bsum_num_of_is_max4	data()[83]	4.063s	passed
bsum_num_of_lt_max	data()[84]	4.045s	passed
bsum_num_of_lt_max2	data()[85]	3.931s	passed
bsum_num_of_lt_max3	data()[86]	3.841s	passed
bsum_num_of_lt_max4	data()[87]	3.881s	passed
bsum_num_of_gt0	data()[88]	3.912s	passed
bsum_num_of_gt0_alt	data()[89]	3.990s	passed
moduloLongIsInLong	data()[8]	4.131s	passed
bsum_add_concrete	data()[90]	3.832s	passed
bprod_all_positive	data()[91]	3.819s	passed
bprod_split	data()[92]	3.853s	passed
powConcrete0	data()[93]	3.822s	passed
powConcrete1	data()[94]	4.014s	passed
powSplitFactor	data()[95]	3.841s	passed
powAdd	data()[96]	3.887s	passed
powMono	data()[97]	3.812s	passed
powMonoConcrete	data()[98]	3.857s	passed
powMonoConcreteRight	data()[99]	3.782s	passed
moduloShortIsInShort	data()[9]	4.172s	passed
Standard output

825        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
859        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 13.94ms 
1183       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1201       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)

2610       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2612       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2614       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2614       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4836       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11754      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.57s 
11830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11875      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.5ns 
11889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11890      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.4ns 
11894      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15621      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 
15624      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16774      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.08ms 
16785      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16785      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.2ns 
16787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20270      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
20271      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21371      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21387      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.35ms 
21391      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21391      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154ns 
21393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24851      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
24852      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25955      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.32ms 
25963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25963      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 431.4ns 
25967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29224      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
29225      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30263      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
30267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.02ms 
30271      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
33312      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34292      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34380      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.82ms 
34382      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34382      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.2ns 
34386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
37450      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
38475      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.42ms 
38479      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
38479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.1ns 
38480      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41514      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
41515      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42483      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
42487      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 792.51ns 
42491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
42491      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.9ns 
42493      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45577      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
45577      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
46619      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 920.01ns 
46623      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
46623      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439ns 
46624      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49794      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
49795      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50789      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
50793      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 786.31ns 
50796      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
50802      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.12ms 
50803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53922      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
53923      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
54964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
54972      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
54976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
54977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.5ns 
54980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
58022      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
58971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
58974      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.21ns 
58979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
58979      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 449ns 
58990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62175      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
62176      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
63173      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
63222      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.28ms 
63229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
63230      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 954.01ns 
63233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66266      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
66266      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
67241      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
67307      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.84ms 
67309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
67309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.8ns 
67312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70341      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
70342      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
71330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
71503      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 162.03ms 
71506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
71506      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.1ns 
71508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74525      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
74525      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
75515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
75521      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
75523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
75523      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.8ns 
75524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78582      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
78582      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
79573      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
79578      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
79582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
79583      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 417.7ns 
79584      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
82576      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
83553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
83609      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.79ms 
83612      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
83613      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.9ns 
83614      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
86664      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
87632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
87652      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.32ms 
87654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
87654      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.5ns 
87655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90669      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
90669      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
91648      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
91665      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.48ms 
91668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
91668      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.9ns 
91669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94708      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
94708      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
95668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
95687      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.34ms 
95690      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
95690      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.9ns 
95692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98729      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
98729      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
99705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
99736      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.46ms 
99742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
99744      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.98ms 
99746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
102766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
103774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
103799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ms 
103800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
103801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
103801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
106821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
107773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
107778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
107781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
107781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.4ns 
107782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
110762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
111726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
111786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.79ms 
111788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
111788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 538.2ns 
111790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
114862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
115835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
115905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.5ms 
115909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
115909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.5ns 
115911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
118896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
119875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
119924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.14ms 
119927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
119929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.14ms 
119931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
123039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
123987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
123997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.28ms 
123999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
123999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns 
124000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
127030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
128009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
128025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
128027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
128027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.3ns 
128028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
131133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
132123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
132138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.92ms 
132140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
132140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.7ns 
132142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
135260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
136273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
136287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.42ms 
136292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
136292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.8ns 
136294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
139365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
140351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
140361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ms 
140363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
140363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.8ns 
140365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
143378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
144337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
144346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.47ms 
144348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
144348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.7ns 
144349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
147342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
148311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
148315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
148317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
148317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.5ns 
148318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
151373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
152309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
152321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.63ms 
152323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
152323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.8ns 
152324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
155380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
156330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
156380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.01ms 
156383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
156383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 418.5ns 
156385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
159353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
160288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
160310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.84ms 
160313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
160313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.3ns 
160315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
163309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
164270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
164289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.45ms 
164291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
164291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.6ns 
164292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
167252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
168217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
168236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.09ms 
168238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
168238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
168239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
171203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
172146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
172164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.64ms 
172166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
172166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
172167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
175147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
176098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
176147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.4ms 
176149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
176149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
176151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
179131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
180120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
180129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
180131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
180131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.2ns 
180132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
183130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
184107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
184112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
184114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
184114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
184115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
187089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
188010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
188020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
188021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
188021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
188022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
190961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
191920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
191929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.13ms 
191931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
191931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
191932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
194913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
195878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
195907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.64ms 
195915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
195916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.3ns 
195917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
198900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
199853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
199862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms 
199864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
199864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
199866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
202812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
203805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
203808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
203810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
203810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.5ns 
203812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
206835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
207791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
207795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
207796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
207796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
207797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
210732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
211695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
211700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
211710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
211710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.1ns 
211711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
214773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
215715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
215847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 122.34ms 
215850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
215851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369ns 
215852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
218907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
219894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
219997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.83ms 
219999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
219999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.5ns 
220000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
223019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
223951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
223955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
223957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
223957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
223958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
227048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
228050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
228129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.5ms 
228134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
228142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.19ms 
228143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
231236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
232245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
232282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.52ms 
232284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
232284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.2ns 
232285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
235438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
236440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
236443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
236446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
236446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.4ns 
236448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
239503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
240491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
240646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 142.67ms 
240649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
240649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.5ns 
240650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
243865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
244879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
244891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
244892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
244892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
244893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
247993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
249003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
249013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.58ms 
249015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
249015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.3ns 
249016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
252158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
253190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
253224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.55ms 
253227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
253228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.1ns 
253233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
256377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
257386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
257404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.77ms 
257413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
257413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 418.7ns 
257415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
260545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
261511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
261516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
261517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
261517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
261518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
264625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
265624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
265629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
265630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
265630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
265631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
268665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
269658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
269690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.06ms 
269701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
269701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.6ns 
269707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
272854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
273860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
273879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.86ms 
273880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
273881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
273882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
276956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
277939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
277956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms 
277959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
277959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.4ns 
277960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
280963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
281906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
281910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
281912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
281912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
281912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
284899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
285844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
285848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
285850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
285850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
285851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
288830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
289757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
289763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
289765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
289765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
289766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
292746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
293711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
293714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
293717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
293717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.6ns 
293718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
296641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
297553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
297556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 613.5ns 
297558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
297558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.8ns 
297559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
300452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
301387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
301391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
301393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
301393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
301394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
304305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
305232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
305235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
305237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
305237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.5ns 
305238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
308208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
309184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
309253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.81ms 
309255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
309255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
309256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
312268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
313235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
313277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.72ms 
313282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
313282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
313283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
316221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
317195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
317243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.71ms 
317244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
317244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
317245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
320199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
321131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
321181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.15ms 
321184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
321184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
321185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
324117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
325025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
325059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.18ms 
325061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
325061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.8ns 
325062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
328097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
329098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
329164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.7ms 
329166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
329167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.8ns 
329168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
332381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
333359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
333390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.76ms 
333393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
333393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.6ns 
333394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
336428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
337405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
337431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.64ms 
337432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
337433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
337434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
340514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
341530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
341555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.72ms 
341556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
341557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
341558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
344627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
345595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
345614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.98ms 
345615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
345616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
345616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
348671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
349653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
349678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.45ms 
349679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
349679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
349680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
352734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
353698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
353722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.02ms 
353724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
353724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
353725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
356678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
357629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
357653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.74ms 
357655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
357655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
357656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
360544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
361473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
361494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.06ms 
361496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
361496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
361497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
364427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
365352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
365375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.53ms 
365377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
365377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
365378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
368320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
369269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
369288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.12ms 
369289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
369289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
369290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
372313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
373255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
373277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.73ms 
373279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
373279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
373280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
376164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
377102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
377110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.58ms 
377111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
377111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
377112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
379978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
380913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
380929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ms 
380930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
380930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
380931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
383839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
384777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
384781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
384783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
384783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
384783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
387688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
388601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
388604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 891.8ns 
388605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
388605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.8ns 
388606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
391668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
392615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
392617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840ns 
392619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
392619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
392620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
395552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
396450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
396459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
396460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
396460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
396461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
399367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
400338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
400345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
400346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
400346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
400347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
403220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
404144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
404157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.06ms 
404159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
404159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
404160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
407037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
408011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
408015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
408016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
408016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
408017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
410879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
411793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
411796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 602.7ns 
411797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
411797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
411798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
414739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
415684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
415694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
415696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
415696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
415697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
418705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
419681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
419684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
419685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
419686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
419686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
422555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
423478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
423481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 753.6ns 
423482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
423482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
423483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
426396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
427326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
427328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.6ns 
427330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
427330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
427330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
430158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
431135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
431140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
431141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
431141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
431142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
434068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
434991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
435000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.79ms 
435002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
435002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
435003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
437882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
438853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
438856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
438858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
438858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
438859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
441860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
442787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
442794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
442796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
442796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.4ns 
442797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
445811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
446761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
446766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
446768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
446770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.8ms 
446771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
449699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
450649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
450668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.65ms 
450669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
450669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
450670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
453621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
454557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
454561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
454562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
454562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
454563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
457477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
458404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
458408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
458409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
458409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
458410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
461317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
462315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
462320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
462322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
462322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
462323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
465249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
466179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
466197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
466198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
466198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
466199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
469186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
470121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
470126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 415.8ns 
470128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
470128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
470129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
473013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
473932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
473975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.25ms 
473976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
473976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
473977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
476859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
477766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
477769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
477772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
477772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
477773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
480669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
481606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
481627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.37ms 
481630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
481630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.7ns 
481631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
484526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
485455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
485475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.79ms 
485476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
485476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
485477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
488379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
489302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
489329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.35ms 
489331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
489331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
489332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
492255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
493177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
493180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 805ns 
493181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
493181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
493182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
496107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
497008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
497015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
497016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
497017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
497017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
499944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
500863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
500867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
500868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
500868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
500869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
503751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
504684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
504688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
504691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
504691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
504692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
507575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
508492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
508495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 875.9ns 
508496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
508496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
508497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
511431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
512396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
512400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
512401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
512401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.5ns 
512402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
515360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
516328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
516332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
516334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
516334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.7ns 
516336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
519294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
520283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
520294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.92ms 
520296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
520296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
520297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
523373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
524394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
524404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.65ms 
524406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
524406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
524406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
527388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
528371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
528380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
528381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
528381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
528382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
531443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
532410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
532457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
532459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
532459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
532459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
535362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
536308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
536313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
536314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
536314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.7ns 
536315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
539228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
540167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
540172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
540174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
540174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
540175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
543041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
543991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
543994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 986.5ns 
543995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
543995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
543996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
546891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
547854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
547857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
547859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
547859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
547860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
550735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
551675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
551677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
551679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
551679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
551680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
554752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
555762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
555774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.64ms 
555775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
555775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
555776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
558835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
559840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
559844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
559845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
559845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.8ns 
559846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
562965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
564015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
564022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
564023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
564023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
564024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
567143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
568193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
568196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 987.9ns 
568197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
568198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
568198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
571332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
572353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
572356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
572358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
572358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
572359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
575439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
576459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
576462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
576464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
576464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
576465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
579633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
580658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
580662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
580663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
580663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
580664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
583754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
584755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
584759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
584760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
584760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
584761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
587876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
588899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
588903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
588905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
588905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
588905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
592109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
593125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
593130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
593132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
593132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
593132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
596232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
597258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
597262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
597263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
597263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
597264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
600382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
601411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
601423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.43ms 
601424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
601425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
601425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
604559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
605578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
605581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 747.2ns 
605582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
605582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
605583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
608693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
609678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
609686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
609688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
609688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
609689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
612744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
613762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
613766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
613767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
613767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
613768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
616796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
617789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
617792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931.4ns 
617793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
617793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
617794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
620926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
621907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
621912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.66ms 
621914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
621914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
621914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
624990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
625971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
625975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
625976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
625976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
625977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
628995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
630022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
630026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
630028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
630028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
630029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
633058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
634034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
634037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
634038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
634039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
634039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
637063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
638031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
638037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
638038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
638038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
638039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
641082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
642058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
642068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.03ms 
642070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
642070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
642071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
645091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
646103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
646113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.57ms 
646115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
646115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
646116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
649105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
650082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
650090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
650092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
650092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
650093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
653169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
654157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
654165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.19ms 
654167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
654167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
654168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
657218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
658223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
658237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ms 
658239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
658239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
658240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
661226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
662210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
662224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
662225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
662225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
662226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
665199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
666168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
666181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.54ms 
666183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
666183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
666184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
669160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
670134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
670145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.25ms 
670146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
670146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
670147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
673126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
674127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
674155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.59ms 
674157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
674157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
674158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
677123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
678085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
678113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.7ms 
678115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
678115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
678116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
681063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
682002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
682027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.81ms 
682029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
682029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
682030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
684938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
685900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
685926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22ms 
685927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
685927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
685928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
688870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
689848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
689873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.5ms 
689875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
689875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
689876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
692769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
693725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
693794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.8ms 
693796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
693796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.5ns 
693797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
696656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
697604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
697610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
697611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
697611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
697612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
700512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
701477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
701483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
701485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
701485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
701485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
704360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
705293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
705297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
705299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
705299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
705300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
708159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
709102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
709121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.71ms 
709124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
709124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 939.2ns 
709124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
712010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
712972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
712980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 
712989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
712989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
712990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
715899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
716841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
716845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
716846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
716846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
716847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
719767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
720741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
720754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.21ms 
720755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
720755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.5ns 
720756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
723768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
724746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
724761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms 
724763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
724763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
724764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
727764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
728756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
728777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.73ms 
728779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
728780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321ns 
728781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
731857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
732830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
732833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
732835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
732835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
732835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
735730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
736682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
736686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
736688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
736688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164ns 
736689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
739611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
740549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
740557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.44ms 
740558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
740558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
740559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
743407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
744342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
744348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
744349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
744349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
744350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
747211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
748143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
748208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.43ms 
748211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
748211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
748212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
751089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
751089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
752030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
752055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.1ms 
752056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
752056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
752057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
754932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
755870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
755887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.07ms 
755889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
755889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.3ns 
755890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
758756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
759698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
759700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 361.7ns 
759701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
759701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
759703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
762625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
763571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
763684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.26ms 
763686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
763693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.35ms 
763694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
766620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
767557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
767604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.34ms 
767605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
767605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
767606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
770488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
771431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
771434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 397.5ns 
771437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
771437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.6ns 
771437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
774468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
775459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
775462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.6ns 
775463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
775463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
775464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
778451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
779408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
779410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 394.2ns 
779412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
779412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
779413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
782395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
783360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
783362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 529.8ns 
783364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
783364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
783365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
786416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
787432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
787554     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
787568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 132.95ms 
787571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
787571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.5ns 
787573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
790678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
790679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
791664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
791717     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
791718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.52ms 
791720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
791720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
791721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
794694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
794694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
795954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
795956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
796002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
796064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
796095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
796106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
796133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
796135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
796137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
796143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
796148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
796154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
796163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
796172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
796503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
796505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
796507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
796508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
796510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
796849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
796850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
796854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
796855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
796857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
796867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
797091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
797093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
797094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
797095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
797095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
797097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
797264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
797265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
797267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
797268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
797269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
797270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
797280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
797281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
797283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
797284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
797285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
797286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
797296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
797297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
797298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
797299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
797300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
797301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
797478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
797479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
797480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
797639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
797640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
797642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
797644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
797645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
797646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
797647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
797648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
797653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
797654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
797656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
797657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
797658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
797797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
797802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
797803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
797804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
797805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
797806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
797807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
797965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
797967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
797968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
797970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
797971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
797972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
797973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
797974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
798108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
798109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
798236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
798242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
798249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
798250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
798251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
798252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
798253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
798254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
798258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
798259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
798270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
798277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
798415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
798416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
798418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
798419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
798420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
798421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
798422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
798422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
798517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
798526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
798707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
798708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
798710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
798712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
798714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
798715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
798901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
798907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
798910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
798912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
798914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
798918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
798919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
798920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
798937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
798945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
798947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
798948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
799084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
799086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
799087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
799089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
799089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
799091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
799234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
799236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
799238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
799239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
799240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
799241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
799242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
799243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
799349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
799351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
799500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
799501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
799502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
799508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
799512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
799518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
799720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
799721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
799722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
799724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
799739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
799853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
804644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
804645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
804649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
804651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
804651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
804652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
804652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
804663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
804664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
804665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
804666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
804667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
804786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
804791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
804793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
804794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
804795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
804795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
804796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
804952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
804953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
804954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
804956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
804956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
804957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
804958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
804958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
805057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
805058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
805161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
805166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
805172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
805173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
805174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
805175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
805191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
805297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
805298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
805299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
805300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
805394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
805407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
805407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
805408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
805410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
805410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
805411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
805412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
805425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
805426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
805427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
805428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
805429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
805545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
805546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
805547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
805548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
805549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
805667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
805673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
805674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
805675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
805675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
805676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
805677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
805808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
805809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
805810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
805811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
805812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
805812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
805813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
805814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
805814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
805815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
805816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
805817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
805817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
805818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
805819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
805933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
805934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
805942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
806044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
806147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
806148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
806149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
806150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
806151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
806151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
806152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
806152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
806153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
806264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
806273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
806387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
806388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
806388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
806389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
806390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
806390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
806391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
806392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
806399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
806400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
806505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
806512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
806521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
806657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
806658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
806659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
806660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
806661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
806662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
806662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
806663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
806737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
806738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
806740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
806742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
806743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
806752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
806759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
806908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
807027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
807028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
807029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
807030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
807282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
807396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
807397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
811096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
811101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
811103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
811103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
811104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
811305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
811306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
811307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
811308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
811309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
811446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
815070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
818911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
818916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
818917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
818918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
818919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
819057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
819057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
819058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
819059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
819060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
820476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
820476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
820477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
823471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
824445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
824447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
824447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
824455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
824468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
824470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
824473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
824475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
824481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
824481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
824486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
824487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
824490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
824500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
824501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
824502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
824558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
824558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
824559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
824560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
824560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
824635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
824636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
824637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
824637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
824638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
824642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
824643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
824643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
824644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
824645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
824646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
824739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
824740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
824740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
824741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
824742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
824743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
824842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
824843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
824843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
824844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
824844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
824845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
824846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
824846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
824847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
824848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
824848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
824848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
824849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
824849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
824850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
824850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
824851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
824851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
824852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
824855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
824901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
824902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
824973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
824973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
824974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
824975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
824976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
824977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
825033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
825035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
825036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
825037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
825038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
825039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
825040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
825090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
825093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
825096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
825158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
825224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
825224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
825225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
828229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
828229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
829248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
829271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.78ms