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

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
198
tests
failures
ignored
14m2.04s
duration
100%
successful
Tests
Standard output
Tests

Test	Method name	Duration	Result
powPositive	data()[100]	4.203s	passed
powPositiveConcrete	data()[101]	4.159s	passed
powGeq1Concrete	data()[102]	4.105s	passed
pow2InIntLower	data()[103]	4.226s	passed
pow2InIntUpper	data()[104]	4.092s	passed
logSelfConcrete	data()[105]	4.087s	passed
log1Concrete	data()[106]	4.187s	passed
logProduct	data()[107]	4.108s	passed
logTimesBaseConcrete	data()[108]	4.044s	passed
logProdIdentity	data()[109]	4.179s	passed
moduloByteIsInByte	data()[10]	4.310s	passed
logProdIdentityConcrete	data()[110]	4.261s	passed
logPowIdentity	data()[111]	4.121s	passed
logPowIdentityConcrete	data()[112]	4.058s	passed
logPositive	data()[113]	4.204s	passed
logPositiveConcrete	data()[114]	4.175s	passed
logMono	data()[115]	4.095s	passed
logMonoConcrete	data()[116]	4.052s	passed
powLogLess	data()[117]	4.127s	passed
powLogMore2	data()[118]	4.217s	passed
logLessThanPow	data()[119]	4.068s	passed
moduloCharIsInChar	data()[11]	4.228s	passed
logLessThanPowConcrete	data()[120]	4.077s	passed
logSqueeze	data()[121]	4.087s	passed
ifthenelse_equals	data()[122]	4.090s	passed
ifthenelse_equals_1	data()[123]	4.034s	passed
ifthenelse_equals_2	data()[124]	4.023s	passed
disjointWithSingleton1	data()[125]	4.059s	passed
disjointWithSingleton2	data()[126]	4.041s	passed
disjointArrayRanges	data()[127]	4.045s	passed
disjointArrayRangeAllFields1	data()[128]	4.088s	passed
disjointArrayRangeAllFields2	data()[129]	4.123s	passed
div_unique1	data()[12]	4.240s	passed
seqSelfDefinition	data()[130]	4.159s	passed
seqOutsideValue	data()[131]	4.065s	passed
castedGetAny	data()[132]	4.051s	passed
seqGetAlphaCast	data()[133]	4.034s	passed
getOfSeqSingleton	data()[134]	4.060s	passed
getOfSeqSingletonConcrete	data()[135]	4.049s	passed
getOfSeqConcat	data()[136]	4.165s	passed
getOfSeqSub	data()[137]	4.022s	passed
getOfSeqReverse	data()[138]	4.040s	passed
lenOfSeqEmpty	data()[139]	4.104s	passed
div_unique2	data()[13]	4.156s	passed
lenOfSeqSingleton	data()[140]	4.018s	passed
lenOfSeqConcat	data()[141]	4.035s	passed
lenOfSeqSub	data()[142]	4.025s	passed
lenOfSeqReverse	data()[143]	4.107s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	4.043s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	4.047s	passed
getOfSeqSingletonEQ	data()[146]	4.030s	passed
getOfSeqConcatEQ	data()[147]	4.071s	passed
getOfSeqSubEQ	data()[148]	4.052s	passed
getOfSeqReverseEQ	data()[149]	4.076s	passed
div_exists	data()[14]	4.238s	passed
lenOfSeqEmptyEQ	data()[150]	4.027s	passed
lenOfSeqSingletonEQ	data()[151]	4.120s	passed
lenOfSeqConcatEQ	data()[152]	4.103s	passed
lenOfSeqSubEQ	data()[153]	4.067s	passed
lenOfSeqReverseEQ	data()[154]	4.041s	passed
getOfSeqDefEQ	data()[155]	4.016s	passed
lenOfSeqDefEQ	data()[156]	4.071s	passed
seqConcatWithSeqEmpty1	data()[157]	4.042s	passed
seqConcatWithSeqEmpty2	data()[158]	4.148s	passed
seqReverseOfSeqEmpty	data()[159]	4.285s	passed
div_one	data()[15]	4.091s	passed
subSeqComplete	data()[160]	4.390s	passed
subSeqTailR	data()[161]	4.350s	passed
subSeqTailL	data()[162]	4.217s	passed
subSeqTailEQR	data()[163]	4.267s	passed
subSeqTailEQL	data()[164]	4.280s	passed
seqDef_split	data()[165]	4.206s	passed
seqDef_induction_upper	data()[166]	4.187s	passed
seqDef_induction_upper_concrete	data()[167]	4.193s	passed
seqDef_induction_lower	data()[168]	4.123s	passed
seqDef_induction_lower_concrete	data()[169]	4.173s	passed
jdiv_one	data()[16]	4.186s	passed
seqDef_split_in_three	data()[170]	4.220s	passed
seqDef_empty	data()[171]	4.064s	passed
seqDef_one_summand	data()[172]	4.167s	passed
seqDef_lower_equals_upper	data()[173]	4.297s	passed
seqDefOfSeq	data()[174]	4.285s	passed
seqSelfDefinitionEQ2	data()[175]	4.117s	passed
indexOfSeqSingleton	data()[176]	4.193s	passed
indexOfSeqConcatFirst	data()[177]	4.178s	passed
indexOfSeqConcatSecond	data()[178]	4.066s	passed
indexOfSeqSub	data()[179]	4.150s	passed
div_zero	data()[17]	4.471s	passed
lenOfArray2seq	data()[180]	4.044s	passed
getAnyOfArray2seq	data()[181]	4.070s	passed
getOfArray2seq	data()[182]	4.039s	passed
getAnyOfNPermInv	data()[183]	4.253s	passed
seqNPermRange	data()[184]	4.090s	passed
seqPermTrans	data()[185]	4.091s	passed
seqPermRefl	data()[186]	4.067s	passed
seqPermSplit	data()[187]	4.102s	passed
seqNPermRight	data()[188]	4.146s	passed
seqPermFromSwap	data()[189]	4.215s	passed
divResZero1	data()[18]	4.361s	passed
seqPermTransAlt0	data()[190]	4.161s	passed
seqPermTransAlt1	data()[191]	4.285s	passed
seqPermTransAlt2	data()[192]	4.120s	passed
seqPermTransAlt3	data()[193]	4.175s	passed
seqPermForall	data()[194]	4.163s	passed
seqPermExists	data()[195]	4.368s	passed
schiffl_lemma_2	data()[196]	25.937s	passed
schiffl_thm_1	data()[197]	5.017s	passed
eqSameSeq	data()[198]	4.187s	passed
divResZero2	data()[19]	4.299s	passed
eqTermCut	data()[1]	4.867s	passed
divResOne1	data()[20]	4.346s	passed
divResOne2	data()[21]	4.190s	passed
div_cancel1	data()[22]	4.226s	passed
div_cancel2	data()[23]	4.216s	passed
divAddMultDenom	data()[24]	4.078s	passed
divMinus	data()[25]	4.105s	passed
divMinusDenom	data()[26]	4.213s	passed
divLeastDPos	data()[27]	4.110s	passed
divLeastDNeg	data()[28]	4.100s	passed
divGreatestDPos	data()[29]	4.077s	passed
equivAllRight	data()[2]	4.847s	passed
divGreatestDNeg	data()[30]	4.153s	passed
divIncreasingPos	data()[31]	4.079s	passed
divIncreasingNeg	data()[32]	4.060s	passed
jdiv_zero	data()[33]	4.048s	passed
jdivPulloutMinusNum	data()[34]	4.090s	passed
jdivPulloutMinusDenom	data()[35]	4.154s	passed
jdiv_uniquePosPos	data()[36]	4.099s	passed
jdiv_uniquePosNeg	data()[37]	4.110s	passed
jdiv_uniqueNegPos	data()[38]	4.122s	passed
jdiv_uniqueNegNeg	data()[39]	4.137s	passed
irrflConcrete1	data()[3]	4.623s	passed
jdivMultDenom1	data()[40]	4.094s	passed
jdivMultDenom2	data()[41]	4.050s	passed
mod_geZero	data()[42]	4.117s	passed
mod_lessDenom	data()[43]	4.056s	passed
jmod_NumPos	data()[44]	4.057s	passed
jmod_NumNeg	data()[45]	4.063s	passed
jmod_geZero	data()[46]	4.091s	passed
jmodNumZero	data()[47]	4.201s	passed
jmod_pulloutminusNum	data()[48]	4.054s	passed
jmod_pulloutminusDenom	data()[49]	4.127s	passed
irrflConcrete2	data()[4]	4.344s	passed
jmodUnique1	data()[50]	4.158s	passed
jmodUnique2	data()[51]	4.249s	passed
intDivRem	data()[52]	4.049s	passed
jmodjmod	data()[53]	4.072s	passed
jmodDivisible	data()[54]	4.088s	passed
jmodDivisibleRep	data()[55]	4.034s	passed
jdivAddMultDenom	data()[56]	4.186s	passed
jmodAltZero	data()[57]	4.040s	passed
jmodAddMultDenomZero	data()[58]	4.018s	passed
polyDiv_zero	data()[59]	4.115s	passed
cancel_gtPos	data()[5]	4.400s	passed
polyMod_ltdivDenom	data()[60]	4.344s	passed
bsum_empty	data()[61]	4.153s	passed
bsum_induction_upper	data()[62]	4.025s	passed
bsum_induction_lower	data()[63]	4.053s	passed
bsum_num_of_bounds	data()[64]	4.028s	passed
bsum_num_of_bounds2	data()[65]	4.018s	passed
bsum_induction_upper2	data()[66]	4.063s	passed
bsum_induction_upper_concrete	data()[67]	4.091s	passed
bsum_induction_upper_concrete_2	data()[68]	4.045s	passed
bsum_induction_upper2_concrete	data()[69]	4.036s	passed
cancel_gtNeg	data()[6]	4.202s	passed
bsum_induction_lower_concrete	data()[70]	4.037s	passed
bsum_induction_lower2	data()[71]	4.009s	passed
bsum_induction_lower2_concrete	data()[72]	4.006s	passed
bsum_positive	data()[73]	4.086s	passed
bsum_upper_bound	data()[74]	4.010s	passed
bsum_lower_bound	data()[75]	4.039s	passed
bsum_positive_lower_bound_element	data()[76]	4.101s	passed
bsum_sub_same_index	data()[77]	4.043s	passed
bsum_less_same_index	data()[78]	4.115s	passed
bsum_equal_except_one_index	data()[79]	4.190s	passed
moduloIntIsInInt	data()[7]	4.177s	passed
bsum_num_of_is_max	data()[80]	4.201s	passed
bsum_num_of_is_max2	data()[81]	4.160s	passed
bsum_num_of_is_max3	data()[82]	4.077s	passed
bsum_num_of_is_max4	data()[83]	4.075s	passed
bsum_num_of_lt_max	data()[84]	4.087s	passed
bsum_num_of_lt_max2	data()[85]	4.188s	passed
bsum_num_of_lt_max3	data()[86]	4.251s	passed
bsum_num_of_lt_max4	data()[87]	4.183s	passed
bsum_num_of_gt0	data()[88]	4.076s	passed
bsum_num_of_gt0_alt	data()[89]	4.118s	passed
moduloLongIsInLong	data()[8]	4.196s	passed
bsum_add_concrete	data()[90]	4.141s	passed
bprod_all_positive	data()[91]	4.013s	passed
bprod_split	data()[92]	4.021s	passed
powConcrete0	data()[93]	4.072s	passed
powConcrete1	data()[94]	4.043s	passed
powSplitFactor	data()[95]	4.038s	passed
powAdd	data()[96]	4.076s	passed
powMono	data()[97]	4.073s	passed
powMonoConcrete	data()[98]	4.118s	passed
powMonoConcreteRight	data()[99]	4.131s	passed
moduloShortIsInShort	data()[9]	4.272s	passed
Standard output

378        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
405        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.55ms 
682        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705        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)

1771       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1775       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1780       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1781       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3535       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10352      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.67s 
10416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10455      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.1ns 
10469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10470      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 747.55ns 
10475      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14048      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
14052      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15297      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15327      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.32ms 
15343      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15343      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 566.84ns 
15345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18999      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
18999      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20186      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.57ms 
20190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20190      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.31ns 
20198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23674      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
23674      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24808      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
24815      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24815      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.93ns 
24818      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28081      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
28082      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
29151      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
29156      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
29160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
29161      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 572.03ns 
29162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32436      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
32436      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
33515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
33557      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.72ms 
33561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
33562      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.23ns 
33564      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36705      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
36706      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
37739      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
37759      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.43ms 
37764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
37765      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.42ms 
37767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40897      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
40898      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
41934      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
41938      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 893.16ns 
41941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
41942      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.93ns 
41943      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45052      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
45052      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
46134      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
46138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
46139      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 697.84ns 
46140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49352      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
49352      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
50408      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 693.14ns 
50411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
50412      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.32ns 
50413      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53662      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
53663      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
54714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
54718      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 724.04ns 
54720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
54721      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.22ns 
54722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57930      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
57930      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
58938      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
58941      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.75ns 
58949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
58949      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.23ns 
58951      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
62094      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
63145      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
63186      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.47ms 
63188      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
63188      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.61ns 
63189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
66295      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
67309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
67341      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.79ms 
67347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
67353      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.54ms 
67355      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
70432      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
71454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
71580      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 115.78ms 
71584      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
71584      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 473.61ns 
71586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74649      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
74650      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
75666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
75672      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
75674      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
75675      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.43ns 
75676      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
78755      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
79853      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
79857      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
79862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
79862      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 466.74ns 
79864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83205      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
83206      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
84287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
84330      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.48ms 
84333      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
84334      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.23ns 
84335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87595      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
87596      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
88677      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
88692      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.62ms 
88695      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
88695      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.52ns 
88697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91922      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
91922      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
92978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
92991      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.02ms 
92993      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
92994      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.42ns 
92995      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96273      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
96273      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
97323      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
97336      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
97339      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
97340      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.62ns 
97341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
100498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
101513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
101526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.85ms 
101530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
101531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 457.63ns 
101532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
104655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
105716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
105753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.19ms 
105756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
105756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.21ns 
105757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
108909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
109965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
109969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
109972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
109972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.42ns 
109974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
113030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
114011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
114047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.98ms 
114050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
114050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.43ns 
114051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
117114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
118101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
118151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.37ms 
118154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
118155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.82ns 
118156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
121293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
122319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
122366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.24ms 
122368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
122368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.41ns 
122369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
125474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
126466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
126475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
126479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
126480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1ms 
126481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
129578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
130562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
130576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.53ms 
130578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
130578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.21ns 
130579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
133619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
134630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
134649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.37ms 
134657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
134658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 847.51ns 
134659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
137783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
138798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
138806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.71ms 
138809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
138809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.52ns 
138811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
141864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
142877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
142886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.39ms 
142889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
142889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.32ns 
142890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
145920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
146938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
146946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.52ms 
146948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
146948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.91ns 
146949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
149979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
150990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
150994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
150995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
150996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.81ns 
150997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
154060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
155063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
155083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.55ms 
155087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
155089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.27ms 
155091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
158148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
159177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
159237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54ms 
159242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
159243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.22ms 
159245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
162280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
163316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
163337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.24ms 
163340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
163340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.12ns 
163342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
166422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
167430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
167448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.99ms 
167450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
167451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.42ns 
167452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
170536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
171552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
171570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.5ms 
171571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
171572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.91ns 
171572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
174635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
175680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
175707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.01ms 
175710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
175710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.72ns 
175712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
178749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
179761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
179801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.17ms 
179803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
179803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.51ns 
179804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
182850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
183844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
183851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
183854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
183854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.82ns 
183855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
186983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
187963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
187968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
187969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
187970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.61ns 
187971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
191030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
192014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
192024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.45ms 
192026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
192027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.22ns 
192028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
195095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
196073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
196082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.14ms 
196083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
196083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.51ns 
196084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
199130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
200106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
200144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.27ms 
200146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
200147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.92ns 
200148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
203214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
204220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
204234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.31ms 
204243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
204246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.02ms 
204248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
207434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
208436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
208440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
208443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
208443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.32ns 
208444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
211486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
212490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
212495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
212497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
212498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.52ns 
212499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
215595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
216618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
216623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
216624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
216624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.61ns 
216625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
219674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
220696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
220780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.25ms 
220786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
220787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.51ns 
220788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
223867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
224932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
225033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.14ms 
225036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
225036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.25ns 
225037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
228067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
229073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
229082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.16ms 
229085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
229085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.12ns 
229087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
232116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
233119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
233153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.16ms 
233156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
233156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 481.73ns 
233157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
236203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
237217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
237242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.76ms 
237243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
237244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.52ns 
237244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
240268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
241273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
241276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 934.26ns 
241277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
241278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.11ns 
241279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
244307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
245321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
245462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 126.61ms 
245464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
245465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.65ns 
245466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
248488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
249492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
249502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.66ms 
249504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
249504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.61ns 
249505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
252524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
253510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
253521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
253522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
253522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.22ns 
253523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
256600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
257618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
257635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.58ms 
257637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
257637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.01ns 
257638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
260915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
261965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
261977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
261981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
261982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.75ns 
261983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
265135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
266128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
266133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
266135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
266136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.74ns 
266137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
269177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
270154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
270158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
270159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
270160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.71ns 
270160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
273168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
274194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
274212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.58ms 
274213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
274213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.31ns 
274214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
277218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
278225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
278239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.17ms 
278241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
278241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.72ns 
278242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
281239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
282243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
282257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.47ms 
282258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
282259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.41ns 
282259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
285311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
286317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
286320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
286322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
286322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.01ns 
286323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
289373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
290407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
290411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
290412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
290412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.81ns 
290413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
293427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
294451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
294456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
294458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
294459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.73ns 
294460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
297461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
298489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
298492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
298494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
298494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.51ns 
298494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
301526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
302527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
302530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 575.96ns 
302531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
302531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.91ns 
302532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
305536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
306534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
306538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
306539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
306540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.61ns 
306540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
309539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
310541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
310544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 815.49ns 
310545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
310545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.11ns 
310546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
313556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
314531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
314630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 95.28ms 
314632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
314633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.03ns 
314634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
317639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
318612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
318641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25ms 
318642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
318642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.11ns 
318643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
321671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
322653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
322679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.98ms 
322682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
322682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.33ns 
322683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
325771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
326745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
326780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.49ms 
326782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
326782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.02ns 
326783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
329826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
330802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
330823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.36ms 
330825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
330825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.81ns 
330826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
333882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
334887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
334937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.47ms 
334940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
334940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.92ns 
334941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
338059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
339107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
339128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.55ms 
339130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
339130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.91ns 
339131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
342297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
343314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
343330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.38ms 
343331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
343331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.61ns 
343332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
346430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
347470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
347490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.54ms 
347491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
347491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.01ns 
347492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
350544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
351550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
351566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.43ms 
351567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
351568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.71ns 
351568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
354584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
355619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
355641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.38ms 
355643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
355643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.01ns 
355644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
358703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
359709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
359728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.39ms 
359730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
359730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.41ns 
359731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
362797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
363889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
363916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.85ms 
363918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
363918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.43ns 
363920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
367108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
368148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
368167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.15ms 
368168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
368169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.61ns 
368169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
371326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
372333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
372350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.96ms 
372351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
372352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.71ns 
372352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
375372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
376399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
376426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.67ms 
376428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
376429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.62ns 
376430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
379490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
380516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
380544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.48ms 
380546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
380547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.53ns 
380548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
383673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
384678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
384685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms 
384687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
384687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.31ns 
384688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
387706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
388684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
388698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.16ms 
388700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
388700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.31ns 
388701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
391735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
392715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
392719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
392721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
392721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.81ns 
392721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
395807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
396788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
396791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.16ns 
396792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
396792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.41ns 
396793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
399848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
400831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
400834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 819.87ns 
400836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
400836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.31ns 
400837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
403884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
404863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
404872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.92ms 
404874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
404874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.71ns 
404875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
407886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
408940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
408947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
408949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
408949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.61ns 
408950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
412002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
413009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
413021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
413023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
413023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.81ns 
413023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
416117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
417136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
417140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
417141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
417141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.41ns 
417142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
420211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
421268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
421271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 583.15ns 
421272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
421272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.61ns 
421273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
424386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
425468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
425474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
425475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
425475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.01ns 
425476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
428598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
429629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
429632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.17ns 
429633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
429633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.51ns 
429634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
432726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
433735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
433737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.55ns 
433738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
433738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.11ns 
433739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
436900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
437961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
437963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 576.95ns 
437965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
437965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.51ns 
437966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
441014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
442050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
442055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
442056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
442056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.51ns 
442057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
445120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
446134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
446142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
446144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
446144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.01ns 
446145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
449282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
450325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
450329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
450330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
450330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.21ns 
450331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
453446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
454430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
454437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
454438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
454438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
454439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
457493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
458477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
458481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
458483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
458483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.51ns 
458484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
461603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
462644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
462660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.23ms 
462661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
462661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.31ns 
462662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
465884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
466917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
466921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
466923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
466923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.61ns 
466924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
470047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
471034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
471042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
471043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
471043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
471044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
474080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
475096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
475101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
475102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
475102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.71ns 
475103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
478221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
479286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
479304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.84ms 
479306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
479306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.21ns 
479307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
482449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
483471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
483478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577.05ns 
483481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
483481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.71ns 
483482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
486538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
487541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
487574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.06ms 
487575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
487576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.11ns 
487576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
490593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
491623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
491626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
491629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
491629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.41ns 
491630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
494717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
495736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
495755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.94ms 
495756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
495756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.51ns 
495757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
498932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
499955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
499971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.45ms 
499973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
499973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.11ns 
499974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
503008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
504015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
504039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.67ms 
504040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
504040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.61ns 
504041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
507108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
508113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
508116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 674.96ns 
508119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
508119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.42ns 
508120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
511176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
512195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
512201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
512205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
512205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.71ns 
512206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
515270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
516290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
516294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
516295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
516295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.41ns 
516296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
519339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
520324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
520327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.27ns 
520328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
520328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
520329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
523364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
524347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
524350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 887.17ns 
524351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
524351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.21ns 
524352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
527419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
528406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
528409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
528411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
528411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
528412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
531459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
532447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
532451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
532452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
532452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.81ns 
532453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
535499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
536486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
536495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.08ms 
536497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
536497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
536498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
539556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
540575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
540583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms 
540587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
540588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.83ns 
540589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
543689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
544701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
544708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.95ms 
544709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
544709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.61ns 
544710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
547824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
548858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
548867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ms 
548869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
548872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.64ms 
548872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
551903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
552927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
552932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
552933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
552933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.11ns 
552934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
555960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
556978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
556983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
556985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
556985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
556985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
559993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
561015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
561018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 878.26ns 
561019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
561019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
561020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
564050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
565074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
565077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
565078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
565078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.31ns 
565079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
568103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
569123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
569126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.58ns 
569129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
569130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.02ns 
569131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
572264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
573282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
573293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.89ms 
573294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
573294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.41ns 
573295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
576295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
577311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
577314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
577316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
577316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
577317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
580308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
581347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
581354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
581355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
581355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.71ns 
581356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
584410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
585454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
585458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
585460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
585460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.61ns 
585461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
588460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
589474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
589476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 698.55ns 
589478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
589478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.11ns 
589479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
592491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
593508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
593511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
593513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
593513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.11ns 
593514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
596517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
597533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
597536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 882.07ns 
597537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
597537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.51ns 
597538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
600610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
601639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
601643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
601645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
601645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.42ns 
601646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
604646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
605684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
605686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
605688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
605688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
605688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
608710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
609728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
609733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
609734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
609734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
609735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
612765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
613761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
613763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 963.27ns 
613765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
613765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
613765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
616825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
617823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
617834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.01ms 
617835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
617835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
617836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
620888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
621884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
621887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 572.44ns 
621888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
621888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.61ns 
621889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
624918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
625956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
625962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
625964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
625964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
625965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
628967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
629987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
629989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 927.47ns 
629991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
629991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
629991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
633074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
634107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
634110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 794.46ns 
634111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
634111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
634112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
637155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
638208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
638212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
638214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
638214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
638215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
641262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
642277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
642279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 951.17ns 
642281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
642281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.51ns 
642282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
645306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
646317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
646320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
646322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
646322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
646322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
649343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
650333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
650336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
650340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
650341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.51ns 
650341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
653379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
654406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
654410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
654412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
654412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.11ns 
654412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
657421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
658444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
658452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.29ms 
658454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
658454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.31ns 
658455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
661564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
662591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
662600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.81ms 
662601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
662602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.41ns 
662602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
665767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
666877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
666885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ms 
666887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
666887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.61ns 
666888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
670160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
671268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
671276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
671277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
671277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.81ns 
671278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
674553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
675614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
675626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ms 
675627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
675627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.91ns 
675628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
678796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
679826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
679842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.62ms 
679843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
679843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
679844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
682998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
684097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
684109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.21ms 
684110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
684111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.41ns 
684111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
687314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
688381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
688389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.86ms 
688391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
688391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.31ns 
688392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
691503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
692566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
692594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.31ms 
692597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
692597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.82ns 
692598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
695697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
696753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
696782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.53ms 
696783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
696783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.61ns 
696784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
699851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
700939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
700974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.32ms 
700977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
700977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.12ns 
700978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
704051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
705075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
705098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.57ms 
705100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
705100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.81ns 
705101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
708152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
709247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
709271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.51ms 
709273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
709273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.51ns 
709274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
712397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
713435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
713491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.78ms 
713493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
713493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.51ns 
713493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
716521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
717545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
717550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
717557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
717558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.22ns 
717559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
720669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
721716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
721722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
721723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
721723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
721724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
724890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
726016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
726020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
726021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
726021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.61ns 
726022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
729211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
730288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
730304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
730306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
730306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
730306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
733391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
734414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
734421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
734423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
734423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
734423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
737555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
738611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
738614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
738615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
738616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
738616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
741747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
742779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
742792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.96ms 
742793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
742793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.21ns 
742794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
745823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
745824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
746846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
746858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.28ms 
746860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
746860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
746861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
749937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
750993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
751009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.01ms 
751010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
751010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.61ns 
751011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
754051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
755049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
755052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 943.26ns 
755053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
755053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.31ns 
755054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
758088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
759118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
759122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
759123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
759123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.11ns 
759124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
762132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
763155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
763161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
763162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
763162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
763163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
766334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
767406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
767414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
767416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
767416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.41ns 
767417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
770430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
771457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
771504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.78ms 
771506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
771506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
771507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
774553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
775575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
775595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.11ms 
775597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
775598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.32ns 
775598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
778624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
779649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
779662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.11ms 
779663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
779663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
779664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
782736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
783762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
783764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 295.32ns 
783766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
783766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.81ns 
783767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
786795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
787816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
787909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.61ms 
787911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
787911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.41ns 
787912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
791053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
792086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
792125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.16ms 
792126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
792126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
792127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
795209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
795209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
796284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
796286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 422.83ns 
796288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
796288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
796288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
799523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
799523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
800569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
800571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 239.41ns 
800573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
800573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.41ns 
800574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
803608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
803608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
804689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
804691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 244.82ns 
804693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
804693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
804694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
807829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
808864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
808866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 377.43ns 
808867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
808868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
808868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
811877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
811877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
812893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
813018     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
813027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 131.39ms 
813031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
813031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.91ns 
813032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
816287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
817345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
817396     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
817398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.27ms 
817399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
817399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.71ns 
817400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
820485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
820485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
821512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
821514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 
821549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
821590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
821605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
821610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
821622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
821623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
821626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
821627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
821632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
821633     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' 
821635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
821637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
821843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
821844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
821846     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' 
821846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
821848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
821971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
821973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
821974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
821975     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' 
821977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
821978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
822154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
822155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
822157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
822158     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' 
822159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
822160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
822292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
822293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
822295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
822296     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' 
822296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
822298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
822305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
822306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
822308     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' 
822309     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' 
822310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
822311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
822319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
822319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
822321     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' 
822321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
822322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
822323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
822507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
822508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
822510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
822704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
822705     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)'' 
822707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
822709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
822710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
822711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
822714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
822715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
822719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
822721     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' 
822723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
822724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
822725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
822842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
822845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
822846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
822848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
822848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
822849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
822854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
822976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
822977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
822978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
822980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
822982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
822982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
822984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
822985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
823091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
823092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
823189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
823194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
823200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
823201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
823204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
823206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
823207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
823207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
823208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
823209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
823218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
823223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
823329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
823330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
823333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
823334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
823335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
823335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
823336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
823337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
823397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
823405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
823513     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]'' 
823514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
823515     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'' 
823516     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'' 
823518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
823519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
823663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
823667     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'' 
823669     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)'' 
823671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
823673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
823674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
823674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
823675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
823685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
823691     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'' 
823692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
823693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
823797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
823798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
823799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
823800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
823801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
823802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
823915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
823916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
823918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
823919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
823920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
823920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
823921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
823921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
824015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
824017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
824109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
824109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
824110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
824115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
824119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
824124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
824285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
824286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
824287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
824288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
824300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
824410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
828673     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'' 
828674     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)'' 
828678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
828680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
828681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
828682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
828683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
828692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
828693     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'' 
828695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
828696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
828697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
828806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
828810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
828811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
828813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
828813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
828814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
828815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
828926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
828927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
828929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
828930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
828931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
828932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
828932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
828933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
829023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
829024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
829111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
829116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
829122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
829123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
829124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
829125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
829137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
829231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
829232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
829234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
829235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
829320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
829332     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'' 
829333     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)'' 
829334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
829335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
829336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
829337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
829338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
829351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
829352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
829353     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'' 
829354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
829355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
829459     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))'' 
829460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
829461     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'' 
829462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
829464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
829571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
829577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
829578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
829579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
829580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
829581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
829582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
829698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
829700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
829701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
829703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
829703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
829704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
829705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
829706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
829707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
829708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
829709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
829710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
829711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
829711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
829712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
829815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
829817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
829824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
829915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
830009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
830011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
830012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
830013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
830014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
830015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
830016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
830016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
830017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
830116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
830124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
830229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
830230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
830231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
830232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
830233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
830234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
830234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
830235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
830241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
830242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
830335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
830342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
830348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
830464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
830465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
830467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
830468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
830469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
830469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
830470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
830470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
830535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
830536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
830537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
830538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
830539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
830547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
830553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
830690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
830794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
830795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
830796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
830797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
831064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
831166     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'' 
831166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
834566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
834571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
834573     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'' 
834574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
834575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
834706     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))'' 
834707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
834708     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'' 
834709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
834710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
834830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
838235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
841842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
841846     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'' 
841847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
841848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
841849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
841980     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))'' 
841980     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'' 
841981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
841982     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)' ...' 
841983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
843336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
843337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.51ns 
843338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
846514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
846514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
847573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
847574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
847575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
847587     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)'' 
847609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
847620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
847626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
847627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
847633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
847633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
847638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
847638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
847641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
847651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
847652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
847654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
847710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
847711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
847712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
847712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
847713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
847784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
847785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
847785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
847786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
847787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
847791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
847792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
847792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
847792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
847793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
847794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
847882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
847883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
847883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
847884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
847885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
847886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
847981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
847981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
847982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
847982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
847983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
847984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
847984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
847985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
847985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
847986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
847986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
847987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
847987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
847987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
847988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
847988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
847989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
847989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
847990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
847993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
848033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
848034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
848097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
848099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
848099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
848101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
848102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
848102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
848159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
848162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
848163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
848164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
848165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
848166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
848167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
848226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
848228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
848232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
848294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
848354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
848354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.71ns 
848355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
851459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
851459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
852518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
852539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.31ms