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

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

Test	Method name	Duration	Result
powPositive	data()[100]	3.213s	passed
powPositiveConcrete	data()[101]	3.213s	passed
powGeq1Concrete	data()[102]	3.238s	passed
pow2InIntLower	data()[103]	3.214s	passed
pow2InIntUpper	data()[104]	3.213s	passed
logSelfConcrete	data()[105]	3.217s	passed
log1Concrete	data()[106]	3.206s	passed
logProduct	data()[107]	3.219s	passed
logTimesBaseConcrete	data()[108]	3.207s	passed
logProdIdentity	data()[109]	3.244s	passed
moduloByteIsInByte	data()[10]	3.282s	passed
logProdIdentityConcrete	data()[110]	3.214s	passed
logPowIdentity	data()[111]	3.216s	passed
logPowIdentityConcrete	data()[112]	3.211s	passed
logPositive	data()[113]	3.220s	passed
logPositiveConcrete	data()[114]	3.212s	passed
logMono	data()[115]	3.253s	passed
logMonoConcrete	data()[116]	3.213s	passed
powLogLess	data()[117]	3.234s	passed
powLogMore2	data()[118]	3.226s	passed
logLessThanPow	data()[119]	3.239s	passed
moduloCharIsInChar	data()[11]	3.267s	passed
logLessThanPowConcrete	data()[120]	3.232s	passed
logSqueeze	data()[121]	3.249s	passed
ifthenelse_equals	data()[122]	3.227s	passed
ifthenelse_equals_1	data()[123]	3.215s	passed
ifthenelse_equals_2	data()[124]	3.212s	passed
disjointWithSingleton1	data()[125]	3.236s	passed
disjointWithSingleton2	data()[126]	3.210s	passed
disjointArrayRanges	data()[127]	3.213s	passed
disjointArrayRangeAllFields1	data()[128]	3.225s	passed
disjointArrayRangeAllFields2	data()[129]	3.261s	passed
div_unique1	data()[12]	3.346s	passed
seqSelfDefinition	data()[130]	3.237s	passed
seqOutsideValue	data()[131]	3.222s	passed
castedGetAny	data()[132]	3.217s	passed
seqGetAlphaCast	data()[133]	3.260s	passed
getOfSeqSingleton	data()[134]	3.222s	passed
getOfSeqSingletonConcrete	data()[135]	3.215s	passed
getOfSeqConcat	data()[136]	3.247s	passed
getOfSeqSub	data()[137]	3.219s	passed
getOfSeqReverse	data()[138]	3.246s	passed
lenOfSeqEmpty	data()[139]	3.213s	passed
div_unique2	data()[13]	3.389s	passed
lenOfSeqSingleton	data()[140]	3.217s	passed
lenOfSeqConcat	data()[141]	3.241s	passed
lenOfSeqSub	data()[142]	3.224s	passed
lenOfSeqReverse	data()[143]	3.207s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.238s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.219s	passed
getOfSeqSingletonEQ	data()[146]	3.241s	passed
getOfSeqConcatEQ	data()[147]	3.220s	passed
getOfSeqSubEQ	data()[148]	3.238s	passed
getOfSeqReverseEQ	data()[149]	3.227s	passed
div_exists	data()[14]	3.491s	passed
lenOfSeqEmptyEQ	data()[150]	3.242s	passed
lenOfSeqSingletonEQ	data()[151]	3.224s	passed
lenOfSeqConcatEQ	data()[152]	3.244s	passed
lenOfSeqSubEQ	data()[153]	3.219s	passed
lenOfSeqReverseEQ	data()[154]	3.234s	passed
getOfSeqDefEQ	data()[155]	3.212s	passed
lenOfSeqDefEQ	data()[156]	3.236s	passed
seqConcatWithSeqEmpty1	data()[157]	3.225s	passed
seqConcatWithSeqEmpty2	data()[158]	3.246s	passed
seqReverseOfSeqEmpty	data()[159]	3.246s	passed
div_one	data()[15]	3.288s	passed
subSeqComplete	data()[160]	3.234s	passed
subSeqTailR	data()[161]	3.246s	passed
subSeqTailL	data()[162]	3.220s	passed
subSeqTailEQR	data()[163]	3.237s	passed
subSeqTailEQL	data()[164]	3.239s	passed
seqDef_split	data()[165]	3.232s	passed
seqDef_induction_upper	data()[166]	3.257s	passed
seqDef_induction_upper_concrete	data()[167]	3.255s	passed
seqDef_induction_lower	data()[168]	3.264s	passed
seqDef_induction_lower_concrete	data()[169]	3.230s	passed
jdiv_one	data()[16]	3.252s	passed
seqDef_split_in_three	data()[170]	3.282s	passed
seqDef_empty	data()[171]	3.233s	passed
seqDef_one_summand	data()[172]	3.213s	passed
seqDef_lower_equals_upper	data()[173]	3.239s	passed
seqDefOfSeq	data()[174]	3.253s	passed
seqSelfDefinitionEQ2	data()[175]	3.240s	passed
indexOfSeqSingleton	data()[176]	3.232s	passed
indexOfSeqConcatFirst	data()[177]	3.225s	passed
indexOfSeqConcatSecond	data()[178]	3.236s	passed
indexOfSeqSub	data()[179]	3.244s	passed
div_zero	data()[17]	3.301s	passed
lenOfArray2seq	data()[180]	3.239s	passed
getAnyOfArray2seq	data()[181]	3.231s	passed
getOfArray2seq	data()[182]	3.237s	passed
getAnyOfNPermInv	data()[183]	3.234s	passed
seqNPermRange	data()[184]	3.266s	passed
seqPermTrans	data()[185]	3.273s	passed
seqPermRefl	data()[186]	3.259s	passed
seqPermSplit	data()[187]	3.236s	passed
seqNPermRight	data()[188]	3.311s	passed
seqPermFromSwap	data()[189]	3.282s	passed
divResZero1	data()[18]	3.294s	passed
seqPermTransAlt0	data()[190]	3.237s	passed
seqPermTransAlt1	data()[191]	3.242s	passed
seqPermTransAlt2	data()[192]	3.233s	passed
seqPermTransAlt3	data()[193]	3.237s	passed
seqPermForall	data()[194]	3.339s	passed
seqPermExists	data()[195]	3.298s	passed
schiffl_lemma_2	data()[196]	22.437s	passed
schiffl_thm_1	data()[197]	4.052s	passed
eqSameSeq	data()[198]	3.366s	passed
divResZero2	data()[19]	3.312s	passed
eqTermCut	data()[1]	3.888s	passed
divResOne1	data()[20]	3.271s	passed
divResOne2	data()[21]	3.264s	passed
div_cancel1	data()[22]	3.280s	passed
div_cancel2	data()[23]	3.275s	passed
divAddMultDenom	data()[24]	3.276s	passed
divMinus	data()[25]	3.309s	passed
divMinusDenom	data()[26]	3.306s	passed
divLeastDPos	data()[27]	3.244s	passed
divLeastDNeg	data()[28]	3.264s	passed
divGreatestDPos	data()[29]	3.254s	passed
equivAllRight	data()[2]	3.656s	passed
divGreatestDNeg	data()[30]	3.242s	passed
divIncreasingPos	data()[31]	3.231s	passed
divIncreasingNeg	data()[32]	3.255s	passed
jdiv_zero	data()[33]	3.245s	passed
jdivPulloutMinusNum	data()[34]	3.234s	passed
jdivPulloutMinusDenom	data()[35]	3.253s	passed
jdiv_uniquePosPos	data()[36]	3.237s	passed
jdiv_uniquePosNeg	data()[37]	3.245s	passed
jdiv_uniqueNegPos	data()[38]	3.247s	passed
jdiv_uniqueNegNeg	data()[39]	3.375s	passed
irrflConcrete1	data()[3]	3.504s	passed
jdivMultDenom1	data()[40]	3.283s	passed
jdivMultDenom2	data()[41]	3.235s	passed
mod_geZero	data()[42]	3.252s	passed
mod_lessDenom	data()[43]	3.226s	passed
jmod_NumPos	data()[44]	3.221s	passed
jmod_NumNeg	data()[45]	3.274s	passed
jmod_geZero	data()[46]	3.236s	passed
jmodNumZero	data()[47]	3.239s	passed
jmod_pulloutminusNum	data()[48]	3.331s	passed
jmod_pulloutminusDenom	data()[49]	3.236s	passed
irrflConcrete2	data()[4]	3.396s	passed
jmodUnique1	data()[50]	3.283s	passed
jmodUnique2	data()[51]	3.339s	passed
intDivRem	data()[52]	3.226s	passed
jmodjmod	data()[53]	3.242s	passed
jmodDivisible	data()[54]	3.257s	passed
jmodDivisibleRep	data()[55]	3.229s	passed
jdivAddMultDenom	data()[56]	3.322s	passed
jmodAltZero	data()[57]	3.284s	passed
jmodAddMultDenomZero	data()[58]	3.234s	passed
polyDiv_zero	data()[59]	3.238s	passed
cancel_gtPos	data()[5]	3.376s	passed
polyMod_ltdivDenom	data()[60]	3.232s	passed
bsum_empty	data()[61]	3.214s	passed
bsum_induction_upper	data()[62]	3.214s	passed
bsum_induction_lower	data()[63]	3.225s	passed
bsum_num_of_bounds	data()[64]	3.261s	passed
bsum_num_of_bounds2	data()[65]	3.253s	passed
bsum_induction_upper2	data()[66]	3.214s	passed
bsum_induction_upper_concrete	data()[67]	3.210s	passed
bsum_induction_upper_concrete_2	data()[68]	3.205s	passed
bsum_induction_upper2_concrete	data()[69]	3.213s	passed
cancel_gtNeg	data()[6]	3.368s	passed
bsum_induction_lower_concrete	data()[70]	3.238s	passed
bsum_induction_lower2	data()[71]	3.214s	passed
bsum_induction_lower2_concrete	data()[72]	3.214s	passed
bsum_positive	data()[73]	3.246s	passed
bsum_upper_bound	data()[74]	3.234s	passed
bsum_lower_bound	data()[75]	3.244s	passed
bsum_positive_lower_bound_element	data()[76]	3.250s	passed
bsum_sub_same_index	data()[77]	3.246s	passed
bsum_less_same_index	data()[78]	3.256s	passed
bsum_equal_except_one_index	data()[79]	3.229s	passed
moduloIntIsInInt	data()[7]	3.332s	passed
bsum_num_of_is_max	data()[80]	3.222s	passed
bsum_num_of_is_max2	data()[81]	3.218s	passed
bsum_num_of_is_max3	data()[82]	3.226s	passed
bsum_num_of_is_max4	data()[83]	3.281s	passed
bsum_num_of_lt_max	data()[84]	3.227s	passed
bsum_num_of_lt_max2	data()[85]	3.223s	passed
bsum_num_of_lt_max3	data()[86]	3.226s	passed
bsum_num_of_lt_max4	data()[87]	3.229s	passed
bsum_num_of_gt0	data()[88]	3.248s	passed
bsum_num_of_gt0_alt	data()[89]	3.255s	passed
moduloLongIsInLong	data()[8]	3.347s	passed
bsum_add_concrete	data()[90]	3.225s	passed
bprod_all_positive	data()[91]	3.245s	passed
bprod_split	data()[92]	3.218s	passed
powConcrete0	data()[93]	3.212s	passed
powConcrete1	data()[94]	3.213s	passed
powSplitFactor	data()[95]	3.222s	passed
powAdd	data()[96]	3.242s	passed
powMono	data()[97]	3.226s	passed
powMonoConcrete	data()[98]	3.215s	passed
powMonoConcreteRight	data()[99]	3.212s	passed
moduloShortIsInShort	data()[9]	3.340s	passed
Standard output

312        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
338        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.24ms 
570        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586        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)

1454       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1456       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1459       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1459       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3028       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8311       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.74s 
8384       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8422       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.2ns 
8436       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8436       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.71ns 
8440       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11282      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
11284      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12316      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.43ms 
12329      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12330      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 448.91ns 
12331      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15058      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
15058      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15970      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15983      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.13ms 
15985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15985      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.3ns 
15986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
18620      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19487      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
19489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19489      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.2ns 
19490      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22036      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
22036      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22878      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22883      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
22885      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22885      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.21ns 
22886      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25418      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
25419      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.21ms 
26261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26261      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.3ns 
26262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28805      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
28806      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29627      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.89ms 
29629      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29629      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124ns 
29630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32131      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
32132      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32959      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 825.62ns 
32960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.4ns 
32962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35477      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
35477      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36303      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36306      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 677.72ns 
36308      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36308      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.1ns 
36309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38800      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
38801      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39642      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39645      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 651.02ns 
39648      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39648      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.61ns 
39650      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42113      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
42113      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42924      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42927      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 668.82ns 
42930      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42930      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.71ns 
42932      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45406      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
45407      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46195      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 689.02ns 
46198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46198      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.41ns 
46199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48697      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
48698      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49541      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.89ms 
49543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49543      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.6ns 
49551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52063      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
52063      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52904      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52930      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.82ms 
52939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52940      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.61ns 
52941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55418      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
55419      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56420      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 157.21ms 
56424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56425      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.91ns 
56426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58898      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
58898      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59710      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
59712      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59712      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.51ns 
59713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62148      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
62149      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62963      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
62966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.51ns 
62968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
65421      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66265      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.61ms 
66267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.01ns 
66269      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68744      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
68744      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69541      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69558      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.55ms 
69565      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.71ns 
69566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
72045      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
72874      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.05ms 
72877      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
72878      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.6ns 
72881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75329      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
75330      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76145      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.74ms 
76147      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76147      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.41ns 
76148      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78593      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
78593      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79397      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79409      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.89ms 
79411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79411      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.21ns 
79412      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81859      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
81859      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82688      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.18ms 
82693      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82694      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 785.22ns 
82695      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
85138      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
85962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
85965      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
85966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
85966      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
85967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88429      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
88430      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89208      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89240      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.12ms 
89243      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89243      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.81ns 
89245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91722      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
91722      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
92501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
92550      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.45ms 
92553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92554      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 659.62ns 
92555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
95023      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
95825      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95857      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.47ms 
95859      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95859      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.3ns 
95860      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98292      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
98293      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
99094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
99101      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
99103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
99103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
99104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
101540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
102348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
102365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.91ms 
102369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
102369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.21ns 
102370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
104810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
105609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
105620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.86ms 
105622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
105622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
105623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
108080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
108855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
108862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
108864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.5ns 
108864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
111309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
112086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
112094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
112096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
112096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.91ns 
112097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
114542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
115342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
115348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
115349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
115350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
115350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
117782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
118590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
118593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
118595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
118595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
118595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
121019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
121817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
121827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.52ms 
121829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.71ns 
121830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
124247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
125044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
125080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.47ms 
125082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
125082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.6ns 
125083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
127503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
128302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
128317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.26ms 
128319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
128319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.8ns 
128319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
130767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
131546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
131562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.46ms 
131564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
131564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.5ns 
131565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
134016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
134792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
134809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
134811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
134811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
134812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
137366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
138165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
138184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.29ms 
138186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
138187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.71ns 
138188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
140630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
141432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
141467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.49ms 
141468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
141469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.9ns 
141469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
143896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
144700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
144703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
144704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
144704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 
144705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
147144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
147951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
147955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
147956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
147956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
147957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
150400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
151173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
151181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
151182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
151182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
151183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
153620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
154394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
154402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.46ms 
154403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
154403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
154404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
156861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
157659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
157676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.98ms 
157677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
157677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.8ns 
157678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
160104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
160904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
160912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ms 
160913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
160913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
160914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
163339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
164147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
164150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
164152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
164153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.61ns 
164154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
166680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
167477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
167481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
167483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
167483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.61ns 
167484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
169908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
170712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
170717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
170720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
170720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.01ns 
170721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
173165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
173941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
174001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.96ms 
174004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
174004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.11ns 
174005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
176468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
177268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
177340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.86ms 
177342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
177343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.41ns 
177344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
179766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
180563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
180566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
180568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
180568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.91ns 
180569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
182983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
183777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
183808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.46ms 
183810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
183810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.11ns 
183811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
186228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
187031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
187065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.5ms 
187067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
187067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
187068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
189496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
190292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
190294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
190296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
190296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.6ns 
190297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
192738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
193511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
193616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.58ms 
193618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
193618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
193619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
196097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
196892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
196900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
196902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
196902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
196903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
199325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
200124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
200134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.22ms 
200136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
200136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
200137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
202562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
203358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
203373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.09ms 
203374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
203374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
203375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
205796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
206591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
206604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
206606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
206606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
206607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
209024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
209815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
209818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
209820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
209820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.2ns 
209821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
212257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
213028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
213032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
213033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
213033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
213034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
215470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
216242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
216257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.33ms 
216258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
216259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
216259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
218701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
219506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
219519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.75ms 
219520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
219520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
219521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
221965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
222759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
222771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.32ms 
222772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
222772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
222773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
225189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
225982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
225985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
225986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
225987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
225987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
228401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
229193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
229196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
229197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
229197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
229198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
231604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
232396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
232401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
232402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
232402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
232403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
234837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
235610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
235613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 905.73ns 
235615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
235615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.81ns 
235616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
238053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
238849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
238851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 501.51ns 
238852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
238853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
238853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
241269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
242062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
242065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
242067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
242067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
242068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
244486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
245277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
245279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.32ns 
245281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
245281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.51ns 
245282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
247697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
248490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
248525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.02ms 
248528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
248528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.31ns 
248529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
250944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
251738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
251759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.87ms 
251760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
251761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
251761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
254210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
254982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
255003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.77ms 
255005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
255005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.91ns 
255006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
257455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
258225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
258253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.93ms 
258255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
258255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
258255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
260689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
261482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
261499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ms 
261500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
261500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
261501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
263927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
264723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
264755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.12ms 
264757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
264757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
264758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
267172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
267966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
267983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.69ms 
267986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
267986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.91ns 
267987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
270400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
271193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
271206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.15ms 
271207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
271207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
271208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
273640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
274410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
274424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.91ms 
274426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
274426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
274427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
276866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
277637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
277650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.81ms 
277651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
277651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
277652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
280121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
280915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
280931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ms 
280932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
280933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
280933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
283348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
284143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
284158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.59ms 
284160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
284160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.7ns 
284160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
286571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
287365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
287382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
287383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
287383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns 
287384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
289796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
290593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
290607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.82ms 
290609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
290609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
290610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
293023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
293819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
293836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.91ms 
293839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
293839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.41ns 
293840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
296297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
297069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
297085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.77ms 
297086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
297086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
297087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
299529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
300324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
300339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms 
300341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
300341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
300341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
302761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
303558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
303564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
303565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
303565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
303566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
306001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
306798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
306809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.39ms 
306810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
306810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
306811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
309229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
310024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
310028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
310029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
310029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
310030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
312442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
313237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
313239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.42ns 
313241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
313241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
313242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
315678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
316450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
316452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.92ns 
316453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
316453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
316454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
318884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
319654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
319667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.63ms 
319678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
319679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.01ns 
319680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
322116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
322911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
322917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
322919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
322919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.91ns 
322920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
325336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
326134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
326144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.14ms 
326146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
326146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.01ns 
326147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
328558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
329356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
329359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
329360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
329360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
329361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
331773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
332568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
332571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 504.12ns 
332572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
332572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
332572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
334985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
335778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
335783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
335784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
335784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
335785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
338219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
338994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
338996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 620.12ns 
338997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
338997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
338998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
341437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
342232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
342234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 521.51ns 
342236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
342236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
342236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
344650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
345447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
345449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 503.51ns 
345450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
345450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
345451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
347863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
348658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
348661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
348662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
348663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
348663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
351078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
351871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
351878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
351879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
351880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
351880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
354286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
355081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
355084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
355086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
355086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
355087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
357520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
358298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
358304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
358305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
358305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
358306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
360735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
361506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
361510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
361511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
361511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
361512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
363944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
364740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
364754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
364756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
364756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.41ns 
364757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
367172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
367965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
367968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
367969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
367969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
367970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
370386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
371182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
371185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 997.53ns 
371186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
371186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
371187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
373593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
374392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
374395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
374397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
374397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
374397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
376804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
377602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
377615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.27ms 
377617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
377617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
377617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
380051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
380822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
380827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 349.31ns 
380829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
380829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
380829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
383261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
384055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
384080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.44ms 
384082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
384082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
384082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
386495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
387290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
387294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
387295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
387295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
387296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
389709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
390510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
390527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.19ms 
390529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
390529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.61ns 
390530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
392945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
393740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
393753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ms 
393756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
393756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.91ns 
393757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
396175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
396974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
396992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.08ms 
396993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
396994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
396994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
399445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
400222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
400224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 545.01ns 
400226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
400226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.01ns 
400227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
402673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
403468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
403473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
403475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
403475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
403476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
405897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
406697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
406700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
406702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
406702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.81ns 
406703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
409114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
409913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
409915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 776.42ns 
409917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
409917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
409917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
412350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
413125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
413127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.42ns 
413129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
413129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
413129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
415557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
416361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
416364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
416365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
416365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
416366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
418772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
419570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
419573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
419575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
419575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
419575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
421979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
422779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
422787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
422788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
422788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
422789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
425227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
426004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
426011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
426012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
426012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
426013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
428468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
429266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
429273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
429274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
429274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
429275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
431696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
432502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
432509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.38ms 
432510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
432512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.21ms 
432513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
434920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
435727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
435731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
435733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
435733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
435733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
438160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
438944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
438949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
438950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
438950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
438951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
441397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
442206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
442208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 781.52ns 
442210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
442210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
442211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
444618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
445428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
445431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 862.62ns 
445432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
445432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
445433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
447860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
448643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
448646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 807.22ns 
448647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
448647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
448648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
451075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
451883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
451892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.73ms 
451893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
451893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
451894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
454300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
455109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
455112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
455113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
455113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
455114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
457540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
458323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
458358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
458359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
458359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
458360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
460763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
461568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
461570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 827.32ns 
461572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
461572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
461572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
463977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
464785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
464787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 663.92ns 
464789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
464789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
464790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
467220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
468026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
468029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
468030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
468030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
468031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
470442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
471250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
471252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 855.52ns 
471253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
471253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
471254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
473674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
474456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
474459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
474460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
474460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
474461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
476887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
477695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
477698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.43ns 
477699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
477699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
477700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
480129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
480913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
480916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
480918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
480918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
480918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
483349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
484155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
484158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 828.22ns 
484159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
484159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
484160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
486564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
487369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
487378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.27ms 
487379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
487379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
487380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
489805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
490613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
490615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 645.62ns 
490616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
490616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
490617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
493030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
493837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
493843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.63ms 
493844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
493844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
493845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
496277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
497082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
497084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 860.62ns 
497086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
497086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
497086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
499498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
500306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
500309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 739.02ns 
500310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
500310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
500311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
502741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
503549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
503552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
503554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
503554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
503554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
505963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
506768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
506771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840.12ns 
506772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
506772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
506773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
509198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
510002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
510005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
510006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
510006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
510007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
512410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
513215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
513217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
513220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
513220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
513221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
515648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
516451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
516455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
516456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
516456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
516457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
518888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
519672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
519679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ms 
519680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
519680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
519681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
522107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
522915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
522925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
522927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
522927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.51ns 
522928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
525359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
526165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
526171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
526172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
526172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
526173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
528593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
529399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
529405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
529407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
529407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
529407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
531836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
532642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
532651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.45ms 
532653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
532653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
532653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
535077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
535861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
535871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.77ms 
535873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
535873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
535873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
538294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
539099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
539108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.94ms 
539110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
539110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
539110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
541537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
542341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
542348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
542349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
542349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
542350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
544775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
545560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
545579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.19ms 
545581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
545581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
545582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
548008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
548814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
548836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.76ms 
548837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
548837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
548838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
551264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
552072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
552091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.49ms 
552094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
552094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.31ns 
552095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
554525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
555309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
555355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.83ms 
555357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
555357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
555358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
557762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
558568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
558586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.12ms 
558587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
558587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
558588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
561015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
561822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
561867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.5ms 
561869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
561869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
561870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
564289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
565095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
565100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
565102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
565102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
565102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
567524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
568308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
568313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
568314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
568314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
568315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
570739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
571547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
571552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
571554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
571555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.31ns 
571555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
573985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
574793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
574806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
574807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
574807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
574808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
577232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
578039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
578045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
578046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
578047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
578047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
580467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
581275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
581277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
581279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
581279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
581279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
583708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
584493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
584502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.23ms 
584504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
584504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
584504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
586920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
587728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
587738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.71ms 
587740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
587740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
587740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
590165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
590970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
590983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.95ms 
590984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
590984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
590985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
593413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
594218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
594221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.23ns 
594223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
594223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
594223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
596644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
597449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
597453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
597454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
597454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
597455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
599874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
600683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
600689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
600690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
600690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
600691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
603114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
603919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
603924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
603925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
603925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
603926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
606362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
607149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
607190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.78ms 
607191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
607191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
607192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
609636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
610444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
610462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.55ms 
610463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
610463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
610464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
612902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
613710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
613721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.79ms 
613723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
613723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
613723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
616148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
616954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
616957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 237.21ns 
616959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
616959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.81ns 
616960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
619384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
620191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
620268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.34ms 
620270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
620270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
620270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
622709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
623518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
623550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.61ms 
623551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
623551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
623552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
625978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
626786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
626788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 223.91ns 
626789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
626789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
626790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
629215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
630027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
630029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 210.61ns 
630030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
630030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
630031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
632450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
633261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
633262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 205.41ns 
633264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
633264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
633264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
635690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
636497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
636499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 325.01ns 
636501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
636501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
636501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
638925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
639733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
639827     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
639838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.67ms 
639841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
639841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.71ns 
639842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
642287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
643094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
643136     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
643136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.6ms 
643138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
643138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
643139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
645571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
646379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
646380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
646410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 49) 
646443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' on goal 3 (script from line 50) 
646456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' on goal 4 (script from line 51) 
646459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' on goal 5 (script from line 52) 
646468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' on goal 11 (script from line 53) 
646469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' on goal 12 (script from line 54) 
646471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' on goal 13 (script from line 55) 
646472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 14 (script from line 56) 
646476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' on goal 16 (script from line 58) 
646477     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) 
646478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' on goal 18 (script from line 60) 
646480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' on goal 19 (script from line 61) 
646700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' on goal 20 (script from line 62) 
646701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' on goal 97 (script from line 63) 
646703     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) 
646703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' on goal 99 (script from line 66) 
646705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' on goal 100 (script from line 67) 
646822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' on goal 101 (script from line 68) 
646823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' on goal 188 (script from line 69) 
646825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' on goal 189 (script from line 71) 
646856     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) 
646858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' on goal 191 (script from line 73) 
646861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' on goal 192 (script from line 74) 
647039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' on goal 193 (script from line 75) 
647040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 310 (script from line 76) 
647041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 311 (script from line 77) 
647042     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) 
647046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' on goal 313 (script from line 80) 
647047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' on goal 314 (script from line 81) 
647187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' on goal 315 (script from line 82) 
647188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 420 (script from line 83) 
647189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 421 (script from line 84) 
647190     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) 
647191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' on goal 423 (script from line 87) 
647192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' on goal 424 (script from line 88) 
647199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' on goal 425 (script from line 89) 
647200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 434 (script from line 90) 
647202     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) 
647203     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) 
647203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' on goal 437 (script from line 94) 
647204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' on goal 438 (script from line 95) 
647212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' on goal 439 (script from line 96) 
647212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' on goal 448 (script from line 97) 
647213     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) 
647214     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) 
647215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' on goal 451 (script from line 101) 
647215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' on goal 452 (script from line 102) 
647356     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) 
647357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' on goal 562 (script from line 105) 
647358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' on goal 563 (script from line 106) 
647487     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) 
647489     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) 
647490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' on goal 676 (script from line 112) 
647492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' on goal 677 (script from line 113) 
647493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' on goal 679 (script from line 114) 
647494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' on goal 681 (script from line 115) 
647494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' on goal 683 (script from line 116) 
647495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 685 (script from line 117) 
647499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' on goal 684 (script from line 119) 
647500     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) 
647501     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) 
647502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' on goal 689 (script from line 122) 
647503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' on goal 690 (script from line 123) 
647616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 691 (script from line 124) 
647620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' on goal 682 (script from line 126) 
647622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' on goal 796 (script from line 127) 
647623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' on goal 797 (script from line 128) 
647624     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) 
647624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' on goal 799 (script from line 130) 
647625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' on goal 800 (script from line 131) 
647755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' on goal 801 (script from line 132) 
647756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' on goal 912 (script from line 133) 
647758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' on goal 913 (script from line 134) 
647759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' on goal 914 (script from line 135) 
647760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' on goal 916 (script from line 136) 
647761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' on goal 917 (script from line 137) 
647761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' on goal 918 (script from line 138) 
647762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' on goal 919 (script from line 139) 
647871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' on goal 920 (script from line 140) 
647872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' on goal 1011 (script from line 141) 
647971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' on goal 1012 (script from line 142) 
647975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' on goal 915 (script from line 143) 
647980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' on goal 680 (script from line 145) 
647981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' on goal 1099 (script from line 146) 
647982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' on goal 1100 (script from line 147) 
647983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' on goal 1101 (script from line 148) 
647984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' on goal 1103 (script from line 149) 
647984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' on goal 1104 (script from line 150) 
647985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' on goal 1105 (script from line 151) 
647986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' on goal 1106 (script from line 152) 
647994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' on goal 1107 (script from line 153) 
647999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' on goal 1102 (script from line 154) 
648109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' on goal 678 (script from line 156) 
648110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' on goal 1225 (script from line 157) 
648111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' on goal 1226 (script from line 158) 
648112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' on goal 1227 (script from line 159) 
648113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' on goal 1229 (script from line 160) 
648114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' on goal 1230 (script from line 161) 
648114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' on goal 1231 (script from line 162) 
648115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' on goal 1232 (script from line 163) 
648171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' on goal 1233 (script from line 164) 
648178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' on goal 1228 (script from line 165) 
648280     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) 
648281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' on goal 1397 (script from line 169) 
648282     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) 
648283     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) 
648284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' on goal 1401 (script from line 172) 
648285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' on goal 1402 (script from line 173) 
648426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' on goal 1403 (script from line 174) 
648434     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) 
648436     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) 
648438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' on goal 1536 (script from line 180) 
648439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' on goal 1537 (script from line 181) 
648442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' on goal 1539 (script from line 182) 
648443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' on goal 1541 (script from line 183) 
648444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' on goal 1543 (script from line 184) 
648457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' on goal 1544 (script from line 186) 
648462     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) 
648464     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) 
648465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' on goal 1560 (script from line 189) 
648579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' on goal 1542 (script from line 191) 
648580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' on goal 1667 (script from line 192) 
648582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' on goal 1668 (script from line 193) 
648583     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) 
648583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' on goal 1670 (script from line 195) 
648584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' on goal 1671 (script from line 196) 
648713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' on goal 1672 (script from line 197) 
648715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' on goal 1786 (script from line 198) 
648716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' on goal 1787 (script from line 199) 
648717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' on goal 1788 (script from line 200) 
648718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' on goal 1790 (script from line 201) 
648719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' on goal 1791 (script from line 202) 
648720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' on goal 1792 (script from line 203) 
648721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' on goal 1793 (script from line 204) 
648822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' on goal 1794 (script from line 205) 
648824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' on goal 1885 (script from line 206) 
648942     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) 
648943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' on goal 1968 (script from line 208) 
648944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' on goal 1969 (script from line 209) 
648949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' on goal 1970 (script from line 210) 
648954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' on goal 1789 (script from line 211) 
648960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' on goal 1540 (script from line 212) 
649118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' on goal 1538 (script from line 214) 
649119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' on goal 2097 (script from line 215) 
649120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' on goal 2098 (script from line 216) 
649121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' on goal 2099 (script from line 217) 
649136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' on goal 2100 (script from line 218) 
649240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' on goal 1535 (script from line 220) 
652886     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) 
652887     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) 
652891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' on goal 4268 (script from line 227) 
652893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' on goal 4269 (script from line 228) 
652893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' on goal 4271 (script from line 229) 
652894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' on goal 4273 (script from line 230) 
652895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' on goal 4275 (script from line 231) 
652902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' on goal 4276 (script from line 233) 
652903     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) 
652904     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) 
652905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' on goal 4289 (script from line 236) 
652906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' on goal 4290 (script from line 237) 
652999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' on goal 4291 (script from line 238) 
653003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' on goal 4274 (script from line 240) 
653004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' on goal 4400 (script from line 241) 
653005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' on goal 4401 (script from line 242) 
653006     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) 
653006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' on goal 4403 (script from line 244) 
653007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' on goal 4404 (script from line 245) 
653104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' on goal 4405 (script from line 246) 
653105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' on goal 4521 (script from line 247) 
653106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' on goal 4522 (script from line 248) 
653107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' on goal 4523 (script from line 249) 
653108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' on goal 4525 (script from line 250) 
653109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' on goal 4526 (script from line 251) 
653110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' on goal 4527 (script from line 252) 
653110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' on goal 4528 (script from line 253) 
653188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' on goal 4529 (script from line 254) 
653189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' on goal 4622 (script from line 255) 
653285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' on goal 4623 (script from line 256) 
653290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' on goal 4524 (script from line 257) 
653294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' on goal 4272 (script from line 259) 
653295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' on goal 4713 (script from line 260) 
653296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' on goal 4714 (script from line 261) 
653297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' on goal 4715 (script from line 262) 
653308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' on goal 4716 (script from line 263) 
653396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' on goal 4270 (script from line 265) 
653397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' on goal 4839 (script from line 266) 
653398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' on goal 4840 (script from line 267) 
653399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' on goal 4841 (script from line 268) 
653474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' on goal 4842 (script from line 269) 
653484     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) 
653485     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) 
653486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' on goal 4950 (script from line 276) 
653487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' on goal 4951 (script from line 277) 
653488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' on goal 4953 (script from line 278) 
653489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' on goal 4955 (script from line 279) 
653489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' on goal 4957 (script from line 280) 
653500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' on goal 4958 (script from line 282) 
653501     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) 
653502     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) 
653503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' on goal 4979 (script from line 285) 
653504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' on goal 4980 (script from line 286) 
653595     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) 
653596     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) 
653597     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) 
653598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' on goal 5095 (script from line 290) 
653599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' on goal 5096 (script from line 291) 
653691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' on goal 5097 (script from line 292) 
653696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' on goal 4956 (script from line 294) 
653697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' on goal 5212 (script from line 295) 
653698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' on goal 5213 (script from line 296) 
653698     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) 
653699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' on goal 5215 (script from line 300) 
653700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' on goal 5216 (script from line 301) 
653803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' on goal 5217 (script from line 303) 
653805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' on goal 5337 (script from line 304) 
653806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' on goal 5338 (script from line 305) 
653807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' on goal 5339 (script from line 306) 
653808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' on goal 5341 (script from line 307) 
653809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' on goal 5342 (script from line 308) 
653809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' on goal 5343 (script from line 309) 
653810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' on goal 5344 (script from line 310) 
653811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' on goal 5346 (script from line 311) 
653812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' on goal 5347 (script from line 312) 
653813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' on goal 5348 (script from line 313) 
653813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' on goal 5350 (script from line 314) 
653814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' on goal 5351 (script from line 315) 
653815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' on goal 5352 (script from line 316) 
653815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' on goal 5353 (script from line 317) 
653948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' on goal 5354 (script from line 318) 
653949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' on goal 5463 (script from line 319) 
653955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' on goal 5464 (script from line 320) 
654033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' on goal 5349 (script from line 321) 
654113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' on goal 5345 (script from line 323) 
654114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' on goal 5660 (script from line 324) 
654115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' on goal 5662 (script from line 325) 
654116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' on goal 5663 (script from line 326) 
654117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' on goal 5664 (script from line 327) 
654118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' on goal 5666 (script from line 328) 
654118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' on goal 5667 (script from line 329) 
654119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' on goal 5668 (script from line 330) 
654120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' on goal 5669 (script from line 331) 
654205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' on goal 5670 (script from line 332) 
654211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' on goal 5665 (script from line 333) 
654299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' on goal 5661 (script from line 335) 
654300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' on goal 5887 (script from line 336) 
654301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' on goal 5888 (script from line 337) 
654301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' on goal 5889 (script from line 338) 
654302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' on goal 5891 (script from line 339) 
654302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' on goal 5892 (script from line 340) 
654303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' on goal 5893 (script from line 341) 
654303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' on goal 5894 (script from line 342) 
654308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' on goal 5895 (script from line 343) 
654309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' on goal 5897 (script from line 344) 
654386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' on goal 5898 (script from line 345) 
654391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' on goal 5890 (script from line 346) 
654396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' on goal 5340 (script from line 347) 
654494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' on goal 4954 (script from line 349) 
654495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' on goal 6115 (script from line 350) 
654496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' on goal 6116 (script from line 351) 
654497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' on goal 6117 (script from line 352) 
654497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' on goal 6119 (script from line 353) 
654497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' on goal 6120 (script from line 354) 
654498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' on goal 6121 (script from line 355) 
654498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' on goal 6122 (script from line 356) 
654552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' on goal 6123 (script from line 357) 
654553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' on goal 6193 (script from line 358) 
654554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' on goal 6195 (script from line 359) 
654554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' on goal 6196 (script from line 360) 
654555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' on goal 6197 (script from line 361) 
654561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' on goal 6198 (script from line 362) 
654566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' on goal 6194 (script from line 363) 
654683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' on goal 6118 (script from line 364) 
654772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' on goal 4952 (script from line 366) 
654773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' on goal 6456 (script from line 367) 
654774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' on goal 6457 (script from line 368) 
654774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' on goal 6458 (script from line 369) 
654939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' on goal 6459 (script from line 370) 
655027     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) 
655027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' on goal 6735 (script from line 377) 
658033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' on goal 6735 (script from line 379) 
658037     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) 
658038     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) 
658038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' on goal 8785 (script from line 382) 
658039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' on goal 8786 (script from line 383) 
658153     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) 
658153     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) 
658155     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) 
658155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' on goal 8911 (script from line 387) 
658156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' on goal 8912 (script from line 388) 
658261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' on goal 8913 (script from line 389) 
661210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' on goal 6736 (script from line 396) 
664366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' on goal 6736 (script from line 398) 
664370     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) 
664371     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) 
664372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' on goal 12635 (script from line 401) 
664373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' on goal 12636 (script from line 402) 
664486     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) 
664486     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) 
664487     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) 
664488     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) 
664489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' on goal 12760 (script from line 407) 
665575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
665575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.9ns 
665576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
668121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
668955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
668957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
668957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 50) 
668963     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) 
668972     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) 
668974     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) 
668976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' on goal 13 (script from line 54) 
668977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' on goal 14 (script from line 55) 
668981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' on goal 15 (script from line 56) 
668981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 23 (script from line 57) 
668985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' on goal 27 (script from line 58) 
668985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' on goal 28 (script from line 59) 
668987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' on goal 29 (script from line 60) 
668995     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) 
668996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' on goal 46 (script from line 62) 
668997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' on goal 47 (script from line 63) 
669041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' on goal 48 (script from line 64) 
669042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' on goal 119 (script from line 65) 
669043     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) 
669043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' on goal 121 (script from line 67) 
669044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' on goal 122 (script from line 68) 
669106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' on goal 123 (script from line 69) 
669107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' on goal 203 (script from line 70) 
669107     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) 
669108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' on goal 205 (script from line 72) 
669109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' on goal 206 (script from line 73) 
669112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 207 (script from line 74) 
669113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 215 (script from line 75) 
669113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' on goal 216 (script from line 76) 
669113     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) 
669114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' on goal 218 (script from line 78) 
669115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' on goal 219 (script from line 79) 
669192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 220 (script from line 80) 
669193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 311 (script from line 81) 
669193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' on goal 312 (script from line 82) 
669194     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) 
669195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' on goal 314 (script from line 84) 
669195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' on goal 315 (script from line 85) 
669276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 316 (script from line 86) 
669277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' on goal 410 (script from line 87) 
669277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' on goal 411 (script from line 88) 
669278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' on goal 412 (script from line 89) 
669278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' on goal 413 (script from line 90) 
669279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' on goal 414 (script from line 91) 
669280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' on goal 416 (script from line 92) 
669280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' on goal 417 (script from line 93) 
669281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' on goal 418 (script from line 94) 
669281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' on goal 420 (script from line 95) 
669282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' on goal 421 (script from line 96) 
669282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' on goal 422 (script from line 97) 
669282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' on goal 423 (script from line 98) 
669283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' on goal 424 (script from line 99) 
669283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' on goal 425 (script from line 100) 
669284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' on goal 426 (script from line 101) 
669284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' on goal 427 (script from line 102) 
669285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' on goal 428 (script from line 103) 
669286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' on goal 430 (script from line 104) 
669288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' on goal 431 (script from line 105) 
669323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' on goal 429 (script from line 106) 
669324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 473 (script from line 107) 
669378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' on goal 474 (script from line 108) 
669379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' on goal 541 (script from line 109) 
669380     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) 
669381     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) 
669382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' on goal 545 (script from line 112) 
669383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 546 (script from line 113) 
669432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' on goal 547 (script from line 114) 
669435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' on goal 542 (script from line 115) 
669436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' on goal 606 (script from line 116) 
669437     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) 
669438     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) 
669439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' on goal 610 (script from line 119) 
669440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' on goal 611 (script from line 120) 
669515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' on goal 612 (script from line 121) 
669518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' on goal 607 (script from line 122) 
669521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' on goal 419 (script from line 123) 
669575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' on goal 415 (script from line 124) 
669628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
669628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.71ns 
669629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
672119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
672975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
672991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.75ms