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

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

Test	Method name	Duration	Result
powPositive	data()[100]	3.094s	passed
powPositiveConcrete	data()[101]	3.081s	passed
powGeq1Concrete	data()[102]	3.089s	passed
pow2InIntLower	data()[103]	3.092s	passed
pow2InIntUpper	data()[104]	3.099s	passed
logSelfConcrete	data()[105]	3.106s	passed
log1Concrete	data()[106]	3.085s	passed
logProduct	data()[107]	3.095s	passed
logTimesBaseConcrete	data()[108]	3.093s	passed
logProdIdentity	data()[109]	3.102s	passed
moduloByteIsInByte	data()[10]	3.191s	passed
logProdIdentityConcrete	data()[110]	3.094s	passed
logPowIdentity	data()[111]	3.086s	passed
logPowIdentityConcrete	data()[112]	3.083s	passed
logPositive	data()[113]	3.105s	passed
logPositiveConcrete	data()[114]	3.090s	passed
logMono	data()[115]	3.098s	passed
logMonoConcrete	data()[116]	3.082s	passed
powLogLess	data()[117]	3.100s	passed
powLogMore2	data()[118]	3.101s	passed
logLessThanPow	data()[119]	3.105s	passed
moduloCharIsInChar	data()[11]	3.184s	passed
logLessThanPowConcrete	data()[120]	3.104s	passed
logSqueeze	data()[121]	3.120s	passed
ifthenelse_equals	data()[122]	3.092s	passed
ifthenelse_equals_1	data()[123]	3.088s	passed
ifthenelse_equals_2	data()[124]	3.090s	passed
disjointWithSingleton1	data()[125]	3.094s	passed
disjointWithSingleton2	data()[126]	3.104s	passed
disjointArrayRanges	data()[127]	3.104s	passed
disjointArrayRangeAllFields1	data()[128]	3.108s	passed
disjointArrayRangeAllFields2	data()[129]	3.096s	passed
div_unique1	data()[12]	3.212s	passed
seqSelfDefinition	data()[130]	3.109s	passed
seqOutsideValue	data()[131]	3.107s	passed
castedGetAny	data()[132]	3.102s	passed
seqGetAlphaCast	data()[133]	3.094s	passed
getOfSeqSingleton	data()[134]	3.092s	passed
getOfSeqSingletonConcrete	data()[135]	3.090s	passed
getOfSeqConcat	data()[136]	3.101s	passed
getOfSeqSub	data()[137]	3.096s	passed
getOfSeqReverse	data()[138]	3.110s	passed
lenOfSeqEmpty	data()[139]	3.097s	passed
div_unique2	data()[13]	3.182s	passed
lenOfSeqSingleton	data()[140]	3.097s	passed
lenOfSeqConcat	data()[141]	3.095s	passed
lenOfSeqSub	data()[142]	3.087s	passed
lenOfSeqReverse	data()[143]	3.092s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.088s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.096s	passed
getOfSeqSingletonEQ	data()[146]	3.116s	passed
getOfSeqConcatEQ	data()[147]	3.107s	passed
getOfSeqSubEQ	data()[148]	3.091s	passed
getOfSeqReverseEQ	data()[149]	3.099s	passed
div_exists	data()[14]	3.240s	passed
lenOfSeqEmptyEQ	data()[150]	3.094s	passed
lenOfSeqSingletonEQ	data()[151]	3.110s	passed
lenOfSeqConcatEQ	data()[152]	3.092s	passed
lenOfSeqSubEQ	data()[153]	3.090s	passed
lenOfSeqReverseEQ	data()[154]	3.084s	passed
getOfSeqDefEQ	data()[155]	3.094s	passed
lenOfSeqDefEQ	data()[156]	3.113s	passed
seqConcatWithSeqEmpty1	data()[157]	3.105s	passed
seqConcatWithSeqEmpty2	data()[158]	3.103s	passed
seqReverseOfSeqEmpty	data()[159]	3.123s	passed
div_one	data()[15]	3.141s	passed
subSeqComplete	data()[160]	3.107s	passed
subSeqTailR	data()[161]	3.122s	passed
subSeqTailL	data()[162]	3.118s	passed
subSeqTailEQR	data()[163]	3.146s	passed
subSeqTailEQL	data()[164]	3.121s	passed
seqDef_split	data()[165]	3.164s	passed
seqDef_induction_upper	data()[166]	3.151s	passed
seqDef_induction_upper_concrete	data()[167]	3.133s	passed
seqDef_induction_lower	data()[168]	3.171s	passed
seqDef_induction_lower_concrete	data()[169]	3.126s	passed
jdiv_one	data()[16]	3.127s	passed
seqDef_split_in_three	data()[170]	3.141s	passed
seqDef_empty	data()[171]	3.125s	passed
seqDef_one_summand	data()[172]	3.104s	passed
seqDef_lower_equals_upper	data()[173]	3.112s	passed
seqDefOfSeq	data()[174]	3.104s	passed
seqSelfDefinitionEQ2	data()[175]	3.097s	passed
indexOfSeqSingleton	data()[176]	3.118s	passed
indexOfSeqConcatFirst	data()[177]	3.107s	passed
indexOfSeqConcatSecond	data()[178]	3.120s	passed
indexOfSeqSub	data()[179]	3.107s	passed
div_zero	data()[17]	3.159s	passed
lenOfArray2seq	data()[180]	3.113s	passed
getAnyOfArray2seq	data()[181]	3.110s	passed
getOfArray2seq	data()[182]	3.109s	passed
getAnyOfNPermInv	data()[183]	3.100s	passed
seqNPermRange	data()[184]	3.171s	passed
seqPermTrans	data()[185]	3.109s	passed
seqPermRefl	data()[186]	3.125s	passed
seqPermSplit	data()[187]	3.107s	passed
seqNPermRight	data()[188]	3.191s	passed
seqPermFromSwap	data()[189]	3.145s	passed
divResZero1	data()[18]	3.136s	passed
seqPermTransAlt0	data()[190]	3.083s	passed
seqPermTransAlt1	data()[191]	3.115s	passed
seqPermTransAlt2	data()[192]	3.110s	passed
seqPermTransAlt3	data()[193]	3.090s	passed
seqPermForall	data()[194]	3.195s	passed
seqPermExists	data()[195]	3.167s	passed
schiffl_lemma_2	data()[196]	21.361s	passed
schiffl_thm_1	data()[197]	3.867s	passed
eqSameSeq	data()[198]	3.152s	passed
divResZero2	data()[19]	3.146s	passed
eqTermCut	data()[1]	3.649s	passed
divResOne1	data()[20]	3.151s	passed
divResOne2	data()[21]	3.137s	passed
div_cancel1	data()[22]	3.164s	passed
div_cancel2	data()[23]	3.113s	passed
divAddMultDenom	data()[24]	3.146s	passed
divMinus	data()[25]	3.147s	passed
divMinusDenom	data()[26]	3.169s	passed
divLeastDPos	data()[27]	3.135s	passed
divLeastDNeg	data()[28]	3.112s	passed
divGreatestDPos	data()[29]	3.110s	passed
equivAllRight	data()[2]	3.519s	passed
divGreatestDNeg	data()[30]	3.126s	passed
divIncreasingPos	data()[31]	3.184s	passed
divIncreasingNeg	data()[32]	3.110s	passed
jdiv_zero	data()[33]	3.135s	passed
jdivPulloutMinusNum	data()[34]	3.115s	passed
jdivPulloutMinusDenom	data()[35]	3.150s	passed
jdiv_uniquePosPos	data()[36]	3.128s	passed
jdiv_uniquePosNeg	data()[37]	3.145s	passed
jdiv_uniqueNegPos	data()[38]	3.131s	passed
jdiv_uniqueNegNeg	data()[39]	3.108s	passed
irrflConcrete1	data()[3]	3.447s	passed
jdivMultDenom1	data()[40]	3.137s	passed
jdivMultDenom2	data()[41]	3.104s	passed
mod_geZero	data()[42]	3.129s	passed
mod_lessDenom	data()[43]	3.116s	passed
jmod_NumPos	data()[44]	3.120s	passed
jmod_NumNeg	data()[45]	3.113s	passed
jmod_geZero	data()[46]	3.102s	passed
jmodNumZero	data()[47]	3.146s	passed
jmod_pulloutminusNum	data()[48]	3.120s	passed
jmod_pulloutminusDenom	data()[49]	3.099s	passed
irrflConcrete2	data()[4]	3.336s	passed
jmodUnique1	data()[50]	3.150s	passed
jmodUnique2	data()[51]	3.185s	passed
intDivRem	data()[52]	3.101s	passed
jmodjmod	data()[53]	3.143s	passed
jmodDivisible	data()[54]	3.117s	passed
jmodDivisibleRep	data()[55]	3.100s	passed
jdivAddMultDenom	data()[56]	3.197s	passed
jmodAltZero	data()[57]	3.105s	passed
jmodAddMultDenomZero	data()[58]	3.098s	passed
polyDiv_zero	data()[59]	3.103s	passed
cancel_gtPos	data()[5]	3.283s	passed
polyMod_ltdivDenom	data()[60]	3.191s	passed
bsum_empty	data()[61]	3.085s	passed
bsum_induction_upper	data()[62]	3.086s	passed
bsum_induction_lower	data()[63]	3.097s	passed
bsum_num_of_bounds	data()[64]	3.106s	passed
bsum_num_of_bounds2	data()[65]	3.102s	passed
bsum_induction_upper2	data()[66]	3.104s	passed
bsum_induction_upper_concrete	data()[67]	3.094s	passed
bsum_induction_upper_concrete_2	data()[68]	3.093s	passed
bsum_induction_upper2_concrete	data()[69]	3.084s	passed
cancel_gtNeg	data()[6]	3.231s	passed
bsum_induction_lower_concrete	data()[70]	3.086s	passed
bsum_induction_lower2	data()[71]	3.088s	passed
bsum_induction_lower2_concrete	data()[72]	3.085s	passed
bsum_positive	data()[73]	3.130s	passed
bsum_upper_bound	data()[74]	3.106s	passed
bsum_lower_bound	data()[75]	3.102s	passed
bsum_positive_lower_bound_element	data()[76]	3.115s	passed
bsum_sub_same_index	data()[77]	3.107s	passed
bsum_less_same_index	data()[78]	3.118s	passed
bsum_equal_except_one_index	data()[79]	3.105s	passed
moduloIntIsInInt	data()[7]	3.228s	passed
bsum_num_of_is_max	data()[80]	3.111s	passed
bsum_num_of_is_max2	data()[81]	3.099s	passed
bsum_num_of_is_max3	data()[82]	3.102s	passed
bsum_num_of_is_max4	data()[83]	3.097s	passed
bsum_num_of_lt_max	data()[84]	3.095s	passed
bsum_num_of_lt_max2	data()[85]	3.097s	passed
bsum_num_of_lt_max3	data()[86]	3.108s	passed
bsum_num_of_lt_max4	data()[87]	3.096s	passed
bsum_num_of_gt0	data()[88]	3.102s	passed
bsum_num_of_gt0_alt	data()[89]	3.107s	passed
moduloLongIsInLong	data()[8]	3.174s	passed
bsum_add_concrete	data()[90]	3.091s	passed
bprod_all_positive	data()[91]	3.097s	passed
bprod_split	data()[92]	3.087s	passed
powConcrete0	data()[93]	3.089s	passed
powConcrete1	data()[94]	3.080s	passed
powSplitFactor	data()[95]	3.086s	passed
powAdd	data()[96]	3.083s	passed
powMono	data()[97]	3.092s	passed
powMonoConcrete	data()[98]	3.083s	passed
powMonoConcreteRight	data()[99]	3.091s	passed
moduloShortIsInShort	data()[9]	3.176s	passed
Standard output

355        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
393        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 14.86ms 
591        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604        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)

1547       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1549       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1551       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1552       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2967       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7819       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.23s 
7881       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7914       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.6ns 
7929       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7929       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 523.91ns 
7933       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10614      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
10617      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11538      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11567      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.75ms 
11588      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11589      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 481.51ns 
11590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
14158      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15082      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15104      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.94ms 
15108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15109      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.7ns 
15114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17742      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
17743      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18553      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
18556      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.5ns 
18558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21061      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
21061      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21878      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21889      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.37ms 
21893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21895      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.42ms 
21897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24349      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
24350      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25174      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.45ms 
25177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25178      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.16ms 
25180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27614      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
27614      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28404      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.92ms 
28409      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28409      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.7ns 
28410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
30841      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31629      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31633      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 580.11ns 
31636      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 797.31ns 
31637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34047      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
34048      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34808      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 623.51ns 
34810      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34811      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.7ns 
34812      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37223      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
37224      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37984      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 567.41ns 
37986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37987      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.5ns 
37988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
40415      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41172      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41175      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 612.01ns 
41178      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41181      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.39ms 
41182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
43601      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44360      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.41ns 
44362      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44363      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.1ns 
44364      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46765      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
46766      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47571      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.09ms 
47578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47578      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.7ns 
47579      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49976      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
49976      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50726      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50759      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.57ms 
50760      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50761      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.1ns 
50762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53135      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
53136      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53885      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
53997      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.58ms 
54000      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54001      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.7ns 
54002      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56386      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
56386      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57135      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57139      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
57141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.7ns 
57142      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59514      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
59515      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60266      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
60268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.5ns 
60270      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62643      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
62643      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63425      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.97ms 
63427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63427      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.3ns 
63428      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65802      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
65802      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66549      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66561      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.93ms 
66562      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66562      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
66563      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68950      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
68950      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69708      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
69709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69709      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns 
69710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72085      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
72085      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
72840      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
72857      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.16ms 
72860      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
72860      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.2ns 
72862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75234      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
75235      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
75984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
75995      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.48ms 
75997      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
75998      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320ns 
75999      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78396      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
78397      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79142      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79159      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.51ms 
79161      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79162      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.1ns 
79163      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
81523      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82272      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
82274      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82274      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.4ns 
82275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
84642      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85418      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.14ms 
85420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85420      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.3ns 
85421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
87779      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88565      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.26ms 
88568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88568      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.9ns 
88569      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
90929      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91733      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.24ms 
91737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91739      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.09ms 
91741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94110      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
94110      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94855      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94869      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.96ms 
94870      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94870      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
94876      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97229      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
97229      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
97971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
97982      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
97983      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
97983      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
97984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
100340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
101081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
101091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.29ms 
101092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
101092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
101093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
103465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
104211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
104219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
104220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
106650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
107395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
107402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
107403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
107403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.2ns 
107404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
109764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
110506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
110512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
110513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
110513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
110514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
112893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
113647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
113648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
116012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
116763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.9ns 
116764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
119128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
119878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
119911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.4ms 
119913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
119913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.7ns 
119914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
122280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
123021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
123038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.23ms 
123041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
123042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.36ms 
123044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
125409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
126154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
126184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.51ms 
126186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
126186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.3ns 
126187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
128548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
129291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
129315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.91ms 
129318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
129318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307ns 
129319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
131669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
132410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
132423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.41ms 
132425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
132425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
132425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
134782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
135529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
135559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.05ms 
135562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
135562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.4ns 
135563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
137917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
138658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
138661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.01ns 
138667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
138667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 658.61ns 
138669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
141049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
141789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
141793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
141795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
141796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.21ms 
141797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
144161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
144903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
144909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ms 
144911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
144911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
144911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
147279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
148022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
148029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
148030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
148030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
148031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
150386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
151127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
151143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.75ms 
151144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
151144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
151145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
153497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
154238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
154244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
154246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
154246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
154246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
156597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
157387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
157390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
157392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
157392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304ns 
157393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
159767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
160507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
160510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
160512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
160512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.4ns 
160513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
162867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
163606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
163610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
163611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
163611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
163612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
165965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
166707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
166759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.51ms 
166760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
166761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
166762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
169111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
169851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
169944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.95ms 
169946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
169946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.8ns 
169947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
172276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
173042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
173045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
173046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
173046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.9ns 
173047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
175400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
176162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
176188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.85ms 
176190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
176190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.5ns 
176191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
178519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
179286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
179305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.17ms 
179306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
179307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
179307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
181639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
182403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
182405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 828.41ns 
182407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
182409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.2ns 
182410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
184741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
185501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
185601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.87ms 
185604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
185604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263ns 
185605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
187931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
188698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
188707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.18ms 
188708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
188708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
188711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
191038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
191800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
191806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
191807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
191807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
191808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
194133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
194895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
194909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.02ms 
194910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
194910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
194911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
197239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
198086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
198096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
198101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
198101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 455.31ns 
198102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
200427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
201182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
201185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
201186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
201186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
201187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
203508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
204267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
204271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
204272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
204272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
204273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
206595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
207355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
207368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
207369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
207369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
207370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
209700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
210462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
210473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.43ms 
210474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
210475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
210475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
212800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
213560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
213575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.94ms 
213577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
213577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.5ns 
213578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
215910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
216676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
216679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 972.61ns 
216680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
216680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
216681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
219012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
219771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
219773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
219775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
219775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
219775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
222103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
222862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
222866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
222868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
222868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
222868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
225190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
225948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
225950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 769.71ns 
225952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
225952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
225952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
228275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
229034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
229036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 455.5ns 
229037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
229038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
229038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
231363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
232121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
232124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
232125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
232125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
232126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
234449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
235208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
235210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.21ns 
235211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
235211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
235212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
237547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
238305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
238339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.78ms 
238341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
238341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
238341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
240661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
241421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
241445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.8ms 
241447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
241447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
241447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
243768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
244528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
244547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.38ms 
244549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
244549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
244549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
246874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
247636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
247662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.11ms 
247663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
247663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
247664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
249994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
250753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
250769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.91ms 
250771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
250771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
250772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
253097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
253857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
253887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.42ms 
253888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
253888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
253889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
256216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
256976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
256992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.94ms 
256994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
256994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.5ns 
257004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
259334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
260092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
260104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.08ms 
260105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
260105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
260106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
262425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
263186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
263202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.26ms 
263204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
263205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.2ns 
263206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
265534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
266293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
266304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.86ms 
266305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
266306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
266306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
268626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
269385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
269401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
269402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
269402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
269403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
271722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
272481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
272496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.01ms 
272498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
272498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
272499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
274816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
275577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
275593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.08ms 
275594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
275594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
275595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
277921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
278687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
278701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ms 
278702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
278702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
278703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
281024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
281784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
281797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.42ms 
281799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
281799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
281799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
284119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
284881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
284899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ms 
284900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
284900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
284901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
287230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
287991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
288006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms 
288007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
288007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
288008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
290332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
291092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
291097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
291099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
291099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
291099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
293421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
294183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
294194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.88ms 
294195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
294195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
294196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
296513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
297278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
297282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
297283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
297283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
297283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
299608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
300369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
300371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 488.11ns 
300372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
300372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
300373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
302687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
303448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
303450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 614.41ns 
303451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
303451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
303452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
305770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
306531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
306536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
306537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
306537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
306538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
308855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
309615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
309620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
309622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
309622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.7ns 
309623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
311940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
312701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
312711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
312713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
312713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.7ns 
312714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
315031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
315791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
315794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
315795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
315795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
315796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
318118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
318884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
318886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 396.1ns 
318887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
318887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
318888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
321207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
321971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
321979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
321980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
321980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
321981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
324298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
325058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
325060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 475.9ns 
325061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
325061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
325062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
327387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
328148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
328150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 465.41ns 
328151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
328151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
328152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
330473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
331239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
331241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 503.71ns 
331243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
331243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
331243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
333576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
334337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
334341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
334342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
334342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
334343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
336668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
337435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
337446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ms 
337448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
337448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.8ns 
337449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
339769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
340528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
340532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
340533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
340533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
340534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
342856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
343622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
343627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
343628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
343628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
343629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
345953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
346716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
346719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
346721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
346721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
346721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
349048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
349808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
349821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.88ms 
349823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
349823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
349823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
352151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
352912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
352915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
352916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
352917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
352917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
355238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
355998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
356001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
356002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
356002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
356003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
358321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
359081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
359085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
359086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
359086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
359087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
361412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
362176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
362189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
362191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
362191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.7ns 
362192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
364515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
365275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
365279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 304.8ns 
365281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
365281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
365281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
367597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
368353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
368378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.59ms 
368379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
368379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
368380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
370695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
371455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
371458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
371460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
371460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
371463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
373785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
374545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
374559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.52ms 
374561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
374561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
374561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
376886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
377646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
377660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
377662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
377662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
377662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
379989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
380748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
380766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.81ms 
380767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
380767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
380768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
383097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
383863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
383869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 521.61ns 
383870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
383870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
383871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
386224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
386984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
386989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
386990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
386990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
386991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
389313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
390078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
390081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
390083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
390083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.5ns 
390084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
392404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
393167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
393169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.21ns 
393170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
393171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
393171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
395493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
396257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
396259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686.01ns 
396260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
396260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
396261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
398583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
399351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
399354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
399355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
399355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
399356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
401681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
402455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
402458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 961.71ns 
402459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
402459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
402460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
404781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
405552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
405561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.09ms 
405562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
405563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
405566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
407897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
408663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
408669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 
408670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
408670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
408671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
410993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
411759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
411765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 
411766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
411766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
411767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
414091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
414862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
414874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.66ms 
414876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
414876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.4ns 
414877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
417203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
417977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
417981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
417983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
417983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.3ns 
417984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
420310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
421080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
421083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
421084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
421084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
421085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
423406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
424176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
424178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684.11ns 
424179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
424179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
424179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
426520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
427267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
427269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 882.31ns 
427271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
427271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
427271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
429612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
430358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
430360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 845.61ns 
430361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
430361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
430362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
432705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
433453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
433461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.22ms 
433462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
433462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
433463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
435808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
436554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
436557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
436558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
436558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
436559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
438893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
439661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
439666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
439667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
439667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
439668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
441992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
442761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
442764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 904.11ns 
442765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
442765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
442766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
445091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
445858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
445860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686.51ns 
445862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
445862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
445862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
448183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
448952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
448955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
448956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
448956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
448957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
451273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
452040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
452043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 718.81ns 
452044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
452044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
452044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
454363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
455132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
455135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 913.81ns 
455136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
455136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
455136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
457474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
458220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
458222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.21ns 
458223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
458224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
458224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
460568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
461314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
461318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
461319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
461319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
461320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
463663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
464432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
464434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 751.11ns 
464435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
464435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
464436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
466764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
467534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
467542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.15ms 
467543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
467543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
467544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
469862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
470631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
470633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 455.7ns 
470634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
470634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
470634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
472956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
473727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
473732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
473733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
473733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
473734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
476078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
476823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
476825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 785.01ns 
476826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
476826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
476827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
479165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
479933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
479935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 668.91ns 
479937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
479937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
479937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
482255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
483024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
483027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
483029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
483029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
483029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
485346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
486115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
486118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 814.91ns 
486119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
486119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
486120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
488433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
489199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
489202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
489203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
489203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
489204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
491545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
492292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
492295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
492296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
492296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
492297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
494636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
495405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
495409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
495410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
495410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
495411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
497736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
498506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
498513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
498514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
498514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
498515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
500862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
501608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
501616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
501617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
501617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
501618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
503960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
504733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
504739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
504740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
504740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
504745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
507067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
507840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
507846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
507847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
507847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
507848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
510184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
510958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
510968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.62ms 
510969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
510969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
510970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
513325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
514076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
514086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.71ms 
514088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
514088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
514088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
516450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
517223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
517232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.26ms 
517233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
517233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
517234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
519572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
520346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
520353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
520354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
520355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
520355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
522747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
523498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
523518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.98ms 
523519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
523519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
523520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
525875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
526647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
526668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.87ms 
526670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
526670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
526671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
529004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
529782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
529801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.64ms 
529803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
529803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
529803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
532176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
532953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
532972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.16ms 
532973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
532973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
532974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
535307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
536079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
536098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.37ms 
536099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
536099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
536100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
538442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
539193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
539239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.81ms 
539241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
539241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
539242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
541588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
542360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
542364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
542365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
542365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
542366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
544688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
545463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
545468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
545469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
545469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
545470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
547810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
548578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
548581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
548582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
548582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
548583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
550902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
551672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
551684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ms 
551685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
551685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
551686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
554026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
554775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
554781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ms 
554782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
554782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
554783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
557124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
557897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
557900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
557901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
557901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
557902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
560247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
560996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
561006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.45ms 
561007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
561008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
561008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
563348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
564116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
564127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.96ms 
564128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
564128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
564129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
566472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
567220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
567233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.03ms 
567234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
567234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
567235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
569576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
570344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
570347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 929.61ns 
570348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
570348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
570348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
572705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
573453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
573456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
573458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
573458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
573458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
575793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
576561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
576566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
576567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
576567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
576568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
578913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
579660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
579665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
579666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
579666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
579667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
582026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
582795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
582836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.02ms 
582838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
582838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
582838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
585180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
585927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
585945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.44ms 
585946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
585946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
585947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
588291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
589059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
589070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.73ms 
589071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
589071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
589072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
591406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
592175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
592177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 219ns 
592179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
592179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.7ns 
592181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
594516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
595284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
595367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.4ms 
595372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
595372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.2ns 
595373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
597710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
598483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
598515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.9ms 
598517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
598517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
598517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
600849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
601597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
601599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 173ns 
601600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
601600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
601600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
603938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
604712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
604714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 245.8ns 
604715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
604715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
604716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
607053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
607821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
607823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.5ns 
607824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
607824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
607825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
610145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
610912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
610914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.1ns 
610915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
610915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
610915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
613250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
614018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
614101     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
614108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.09ms 
614110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
614110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
614110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
616468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
617238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
617274     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
617275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.53ms 
617276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
617276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
617277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
619614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
620386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
620387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 
620421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 49) 
620467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' on goal 3 (script from line 50) 
620480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' on goal 4 (script from line 51) 
620487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' on goal 5 (script from line 52) 
620499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' on goal 11 (script from line 53) 
620500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' on goal 12 (script from line 54) 
620502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' on goal 13 (script from line 55) 
620503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 14 (script from line 56) 
620509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' on goal 16 (script from line 58) 
620512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' on goal 17 (script from line 59) 
620514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' on goal 18 (script from line 60) 
620517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' on goal 19 (script from line 61) 
620740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' on goal 20 (script from line 62) 
620741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' on goal 97 (script from line 63) 
620744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' on goal 98 (script from line 65) 
620745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' on goal 99 (script from line 66) 
620746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' on goal 100 (script from line 67) 
620888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' on goal 101 (script from line 68) 
620889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' on goal 188 (script from line 69) 
620893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' on goal 189 (script from line 71) 
620894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' on goal 190 (script from line 72) 
620895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' on goal 191 (script from line 73) 
620897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' on goal 192 (script from line 74) 
621072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' on goal 193 (script from line 75) 
621074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 310 (script from line 76) 
621075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 311 (script from line 77) 
621076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' on goal 312 (script from line 79) 
621077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' on goal 313 (script from line 80) 
621079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' on goal 314 (script from line 81) 
621190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' on goal 315 (script from line 82) 
621192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 420 (script from line 83) 
621193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 421 (script from line 84) 
621194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' on goal 422 (script from line 86) 
621195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' on goal 423 (script from line 87) 
621196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' on goal 424 (script from line 88) 
621241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' on goal 425 (script from line 89) 
621242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 434 (script from line 90) 
621244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' on goal 435 (script from line 91) 
621244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' on goal 436 (script from line 93) 
621245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' on goal 437 (script from line 94) 
621246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' on goal 438 (script from line 95) 
621251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' on goal 439 (script from line 96) 
621252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' on goal 448 (script from line 97) 
621253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' on goal 449 (script from line 98) 
621253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' on goal 450 (script from line 100) 
621254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' on goal 451 (script from line 101) 
621254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' on goal 452 (script from line 102) 
621366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' on goal 453 (script from line 104) 
621367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' on goal 562 (script from line 105) 
621368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' on goal 563 (script from line 106) 
621468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' on goal 564 (script from line 108) 
621468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' on goal 674 (script from line 110) 
621469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' on goal 676 (script from line 112) 
621471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' on goal 677 (script from line 113) 
621472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' on goal 679 (script from line 114) 
621473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' on goal 681 (script from line 115) 
621473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' on goal 683 (script from line 116) 
621474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 685 (script from line 117) 
621477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' on goal 684 (script from line 119) 
621478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' on goal 687 (script from line 120) 
621479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' on goal 688 (script from line 121) 
621480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' on goal 689 (script from line 122) 
621480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' on goal 690 (script from line 123) 
621572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 691 (script from line 124) 
621575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' on goal 682 (script from line 126) 
621576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' on goal 796 (script from line 127) 
621577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' on goal 797 (script from line 128) 
621577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' on goal 798 (script from line 129) 
621578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' on goal 799 (script from line 130) 
621578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' on goal 800 (script from line 131) 
621683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' on goal 801 (script from line 132) 
621684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' on goal 912 (script from line 133) 
621685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' on goal 913 (script from line 134) 
621686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' on goal 914 (script from line 135) 
621687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' on goal 916 (script from line 136) 
621687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' on goal 917 (script from line 137) 
621688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' on goal 918 (script from line 138) 
621688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' on goal 919 (script from line 139) 
621775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' on goal 920 (script from line 140) 
621776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' on goal 1011 (script from line 141) 
621865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' on goal 1012 (script from line 142) 
621869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' on goal 915 (script from line 143) 
621873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' on goal 680 (script from line 145) 
621874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' on goal 1099 (script from line 146) 
621875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' on goal 1100 (script from line 147) 
621876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' on goal 1101 (script from line 148) 
621877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' on goal 1103 (script from line 149) 
621878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' on goal 1104 (script from line 150) 
621878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' on goal 1105 (script from line 151) 
621879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' on goal 1106 (script from line 152) 
621886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' on goal 1107 (script from line 153) 
621890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' on goal 1102 (script from line 154) 
621975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' on goal 678 (script from line 156) 
621976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' on goal 1225 (script from line 157) 
621977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' on goal 1226 (script from line 158) 
621978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' on goal 1227 (script from line 159) 
621978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' on goal 1229 (script from line 160) 
621979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' on goal 1230 (script from line 161) 
621979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' on goal 1231 (script from line 162) 
621980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' on goal 1232 (script from line 163) 
622030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' on goal 1233 (script from line 164) 
622037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' on goal 1228 (script from line 165) 
622129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' on goal 675 (script from line 168) 
622130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' on goal 1397 (script from line 169) 
622131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' on goal 1399 (script from line 170) 
622133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' on goal 1400 (script from line 171) 
622134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' on goal 1401 (script from line 172) 
622135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' on goal 1402 (script from line 173) 
622263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' on goal 1403 (script from line 174) 
622268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' on goal 1398 (script from line 176) 
622268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' on goal 1534 (script from line 178) 
622269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' on goal 1536 (script from line 180) 
622271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' on goal 1537 (script from line 181) 
622271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' on goal 1539 (script from line 182) 
622272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' on goal 1541 (script from line 183) 
622273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' on goal 1543 (script from line 184) 
622282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' on goal 1544 (script from line 186) 
622283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' on goal 1558 (script from line 187) 
622284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' on goal 1559 (script from line 188) 
622285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' on goal 1560 (script from line 189) 
622380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' on goal 1542 (script from line 191) 
622381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' on goal 1667 (script from line 192) 
622382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' on goal 1668 (script from line 193) 
622383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' on goal 1669 (script from line 194) 
622383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' on goal 1670 (script from line 195) 
622384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' on goal 1671 (script from line 196) 
622484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' on goal 1672 (script from line 197) 
622485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' on goal 1786 (script from line 198) 
622486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' on goal 1787 (script from line 199) 
622487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' on goal 1788 (script from line 200) 
622488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' on goal 1790 (script from line 201) 
622489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' on goal 1791 (script from line 202) 
622489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' on goal 1792 (script from line 203) 
622490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' on goal 1793 (script from line 204) 
622570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' on goal 1794 (script from line 205) 
622571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' on goal 1885 (script from line 206) 
622642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' on goal 1886 (script from line 207) 
622642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' on goal 1968 (script from line 208) 
622643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' on goal 1969 (script from line 209) 
622648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' on goal 1970 (script from line 210) 
622651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' on goal 1789 (script from line 211) 
622655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' on goal 1540 (script from line 212) 
622765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' on goal 1538 (script from line 214) 
622766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' on goal 2097 (script from line 215) 
622767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' on goal 2098 (script from line 216) 
622768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' on goal 2099 (script from line 217) 
622778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' on goal 2100 (script from line 218) 
622858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' on goal 1535 (script from line 220) 
626292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' on goal 1535 (script from line 223) 
626293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' on goal 4266 (script from line 225) 
626297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' on goal 4268 (script from line 227) 
626298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' on goal 4269 (script from line 228) 
626299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' on goal 4271 (script from line 229) 
626300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' on goal 4273 (script from line 230) 
626301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' on goal 4275 (script from line 231) 
626308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' on goal 4276 (script from line 233) 
626309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' on goal 4287 (script from line 234) 
626310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' on goal 4288 (script from line 235) 
626311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' on goal 4289 (script from line 236) 
626312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' on goal 4290 (script from line 237) 
626403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' on goal 4291 (script from line 238) 
626407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' on goal 4274 (script from line 240) 
626407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' on goal 4400 (script from line 241) 
626408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' on goal 4401 (script from line 242) 
626409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' on goal 4402 (script from line 243) 
626410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' on goal 4403 (script from line 244) 
626410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' on goal 4404 (script from line 245) 
626502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' on goal 4405 (script from line 246) 
626503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' on goal 4521 (script from line 247) 
626505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' on goal 4522 (script from line 248) 
626506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' on goal 4523 (script from line 249) 
626506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' on goal 4525 (script from line 250) 
626507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' on goal 4526 (script from line 251) 
626508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' on goal 4527 (script from line 252) 
626508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' on goal 4528 (script from line 253) 
626582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' on goal 4529 (script from line 254) 
626583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' on goal 4622 (script from line 255) 
626656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' on goal 4623 (script from line 256) 
626660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' on goal 4524 (script from line 257) 
626665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' on goal 4272 (script from line 259) 
626665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' on goal 4713 (script from line 260) 
626666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' on goal 4714 (script from line 261) 
626667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' on goal 4715 (script from line 262) 
626677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' on goal 4716 (script from line 263) 
626755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' on goal 4270 (script from line 265) 
626756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' on goal 4839 (script from line 266) 
626757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' on goal 4840 (script from line 267) 
626758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' on goal 4841 (script from line 268) 
626828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' on goal 4842 (script from line 269) 
626838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' on goal 4267 (script from line 272) 
626839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' on goal 4948 (script from line 274) 
626839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' on goal 4950 (script from line 276) 
626841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' on goal 4951 (script from line 277) 
626841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' on goal 4953 (script from line 278) 
626842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' on goal 4955 (script from line 279) 
626843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' on goal 4957 (script from line 280) 
626853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' on goal 4958 (script from line 282) 
626854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' on goal 4977 (script from line 283) 
626855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' on goal 4978 (script from line 284) 
626856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' on goal 4979 (script from line 285) 
626857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' on goal 4980 (script from line 286) 
626942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' on goal 4981 (script from line 287) 
626943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' on goal 5093 (script from line 288) 
626944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' on goal 5094 (script from line 289) 
626944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' on goal 5095 (script from line 290) 
626945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' on goal 5096 (script from line 291) 
627035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' on goal 5097 (script from line 292) 
627039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' on goal 4956 (script from line 294) 
627041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' on goal 5212 (script from line 295) 
627042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' on goal 5213 (script from line 296) 
627043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' on goal 5214 (script from line 299) 
627043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' on goal 5215 (script from line 300) 
627044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' on goal 5216 (script from line 301) 
627138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' on goal 5217 (script from line 303) 
627139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' on goal 5337 (script from line 304) 
627140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' on goal 5338 (script from line 305) 
627141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' on goal 5339 (script from line 306) 
627141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' on goal 5341 (script from line 307) 
627142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' on goal 5342 (script from line 308) 
627142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' on goal 5343 (script from line 309) 
627143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' on goal 5344 (script from line 310) 
627144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' on goal 5346 (script from line 311) 
627144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' on goal 5347 (script from line 312) 
627145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' on goal 5348 (script from line 313) 
627146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' on goal 5350 (script from line 314) 
627146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' on goal 5351 (script from line 315) 
627146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' on goal 5352 (script from line 316) 
627147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' on goal 5353 (script from line 317) 
627237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' on goal 5354 (script from line 318) 
627238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' on goal 5463 (script from line 319) 
627245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' on goal 5464 (script from line 320) 
627319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' on goal 5349 (script from line 321) 
627397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' on goal 5345 (script from line 323) 
627398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' on goal 5660 (script from line 324) 
627398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' on goal 5662 (script from line 325) 
627399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' on goal 5663 (script from line 326) 
627400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' on goal 5664 (script from line 327) 
627400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' on goal 5666 (script from line 328) 
627401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' on goal 5667 (script from line 329) 
627401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' on goal 5668 (script from line 330) 
627402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' on goal 5669 (script from line 331) 
627484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' on goal 5670 (script from line 332) 
627490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' on goal 5665 (script from line 333) 
627577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' on goal 5661 (script from line 335) 
627578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' on goal 5887 (script from line 336) 
627579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' on goal 5888 (script from line 337) 
627580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' on goal 5889 (script from line 338) 
627580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' on goal 5891 (script from line 339) 
627581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' on goal 5892 (script from line 340) 
627581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' on goal 5893 (script from line 341) 
627581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' on goal 5894 (script from line 342) 
627586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' on goal 5895 (script from line 343) 
627587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' on goal 5897 (script from line 344) 
627664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' on goal 5898 (script from line 345) 
627669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' on goal 5890 (script from line 346) 
627675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' on goal 5340 (script from line 347) 
627772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' on goal 4954 (script from line 349) 
627772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' on goal 6115 (script from line 350) 
627773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' on goal 6116 (script from line 351) 
627774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' on goal 6117 (script from line 352) 
627774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' on goal 6119 (script from line 353) 
627775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' on goal 6120 (script from line 354) 
627775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' on goal 6121 (script from line 355) 
627776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' on goal 6122 (script from line 356) 
627828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' on goal 6123 (script from line 357) 
627829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' on goal 6193 (script from line 358) 
627829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' on goal 6195 (script from line 359) 
627830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' on goal 6196 (script from line 360) 
627831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' on goal 6197 (script from line 361) 
627836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' on goal 6198 (script from line 362) 
627842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' on goal 6194 (script from line 363) 
627997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' on goal 6118 (script from line 364) 
628081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' on goal 4952 (script from line 366) 
628082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' on goal 6456 (script from line 367) 
628082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' on goal 6457 (script from line 368) 
628083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' on goal 6458 (script from line 369) 
628243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' on goal 6459 (script from line 370) 
628328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' on goal 4949 (script from line 374) 
628328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' on goal 6735 (script from line 377) 
631218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' on goal 6735 (script from line 379) 
631222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' on goal 8783 (script from line 380) 
631223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' on goal 8784 (script from line 381) 
631224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' on goal 8785 (script from line 382) 
631224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' on goal 8786 (script from line 383) 
631335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' on goal 8787 (script from line 384) 
631336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' on goal 8909 (script from line 385) 
631337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' on goal 8910 (script from line 386) 
631337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' on goal 8911 (script from line 387) 
631338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' on goal 8912 (script from line 388) 
631439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' on goal 8913 (script from line 389) 
634350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' on goal 6736 (script from line 396) 
637430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' on goal 6736 (script from line 398) 
637434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' on goal 12633 (script from line 399) 
637435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' on goal 12634 (script from line 400) 
637437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' on goal 12635 (script from line 401) 
637438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' on goal 12636 (script from line 402) 
637549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' on goal 12637 (script from line 403) 
637551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' on goal 12757 (script from line 404) 
637552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' on goal 12758 (script from line 405) 
637553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' on goal 12759 (script from line 406) 
637554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' on goal 12760 (script from line 407) 
638639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
638639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.1ns 
638640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
641056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
641853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
641854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 
641854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 50) 
641863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' on goal 10 (script from line 51) 
641871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' on goal 11 (script from line 52) 
641874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' on goal 12 (script from line 53) 
641876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' on goal 13 (script from line 54) 
641878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' on goal 14 (script from line 55) 
641882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' on goal 15 (script from line 56) 
641883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 23 (script from line 57) 
641887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' on goal 27 (script from line 58) 
641888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' on goal 28 (script from line 59) 
641890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' on goal 29 (script from line 60) 
641900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' on goal 30 (script from line 61) 
641901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' on goal 46 (script from line 62) 
641902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' on goal 47 (script from line 63) 
641955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' on goal 48 (script from line 64) 
641956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' on goal 119 (script from line 65) 
641957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' on goal 120 (script from line 66) 
641957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' on goal 121 (script from line 67) 
641957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' on goal 122 (script from line 68) 
642020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' on goal 123 (script from line 69) 
642020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' on goal 203 (script from line 70) 
642021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' on goal 204 (script from line 71) 
642022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' on goal 205 (script from line 72) 
642022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' on goal 206 (script from line 73) 
642026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 207 (script from line 74) 
642026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 215 (script from line 75) 
642027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' on goal 216 (script from line 76) 
642027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' on goal 217 (script from line 77) 
642028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' on goal 218 (script from line 78) 
642028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' on goal 219 (script from line 79) 
642112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 220 (script from line 80) 
642113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 311 (script from line 81) 
642113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' on goal 312 (script from line 82) 
642114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' on goal 313 (script from line 83) 
642115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' on goal 314 (script from line 84) 
642115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' on goal 315 (script from line 85) 
642202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 316 (script from line 86) 
642202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' on goal 410 (script from line 87) 
642203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' on goal 411 (script from line 88) 
642203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' on goal 412 (script from line 89) 
642204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' on goal 413 (script from line 90) 
642204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' on goal 414 (script from line 91) 
642205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' on goal 416 (script from line 92) 
642205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' on goal 417 (script from line 93) 
642206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' on goal 418 (script from line 94) 
642206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' on goal 420 (script from line 95) 
642207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' on goal 421 (script from line 96) 
642207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' on goal 422 (script from line 97) 
642207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' on goal 423 (script from line 98) 
642208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' on goal 424 (script from line 99) 
642208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' on goal 425 (script from line 100) 
642208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' on goal 426 (script from line 101) 
642209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' on goal 427 (script from line 102) 
642209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' on goal 428 (script from line 103) 
642210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' on goal 430 (script from line 104) 
642212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' on goal 431 (script from line 105) 
642247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' on goal 429 (script from line 106) 
642248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 473 (script from line 107) 
642304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' on goal 474 (script from line 108) 
642305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' on goal 541 (script from line 109) 
642305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' on goal 543 (script from line 110) 
642306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' on goal 544 (script from line 111) 
642307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' on goal 545 (script from line 112) 
642308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 546 (script from line 113) 
642349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' on goal 547 (script from line 114) 
642351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' on goal 542 (script from line 115) 
642352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' on goal 606 (script from line 116) 
642353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' on goal 608 (script from line 117) 
642354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' on goal 609 (script from line 118) 
642355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' on goal 610 (script from line 119) 
642355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' on goal 611 (script from line 120) 
642397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' on goal 612 (script from line 121) 
642400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' on goal 607 (script from line 122) 
642403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' on goal 419 (script from line 123) 
642455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' on goal 415 (script from line 124) 
642505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
642505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
642506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
644854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
645639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
645655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.27ms