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

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

Test	Method name	Duration	Result
powPositive	data()[100]	4.300s	passed
powPositiveConcrete	data()[101]	4.324s	passed
powGeq1Concrete	data()[102]	4.316s	passed
pow2InIntLower	data()[103]	4.309s	passed
pow2InIntUpper	data()[104]	4.384s	passed
logSelfConcrete	data()[105]	4.335s	passed
log1Concrete	data()[106]	4.292s	passed
logProduct	data()[107]	4.235s	passed
logTimesBaseConcrete	data()[108]	4.298s	passed
logProdIdentity	data()[109]	4.305s	passed
moduloByteIsInByte	data()[10]	4.436s	passed
logProdIdentityConcrete	data()[110]	4.243s	passed
logPowIdentity	data()[111]	4.263s	passed
logPowIdentityConcrete	data()[112]	4.340s	passed
logPositive	data()[113]	4.478s	passed
logPositiveConcrete	data()[114]	4.345s	passed
logMono	data()[115]	4.344s	passed
logMonoConcrete	data()[116]	4.361s	passed
powLogLess	data()[117]	4.385s	passed
powLogMore2	data()[118]	4.378s	passed
logLessThanPow	data()[119]	4.394s	passed
moduloCharIsInChar	data()[11]	4.450s	passed
logLessThanPowConcrete	data()[120]	4.378s	passed
logSqueeze	data()[121]	4.439s	passed
ifthenelse_equals	data()[122]	4.431s	passed
ifthenelse_equals_1	data()[123]	4.402s	passed
ifthenelse_equals_2	data()[124]	4.448s	passed
disjointWithSingleton1	data()[125]	4.411s	passed
disjointWithSingleton2	data()[126]	4.470s	passed
disjointArrayRanges	data()[127]	4.379s	passed
disjointArrayRangeAllFields1	data()[128]	4.418s	passed
disjointArrayRangeAllFields2	data()[129]	4.400s	passed
div_unique1	data()[12]	4.547s	passed
seqSelfDefinition	data()[130]	4.392s	passed
seqOutsideValue	data()[131]	4.406s	passed
castedGetAny	data()[132]	4.383s	passed
seqGetAlphaCast	data()[133]	4.434s	passed
getOfSeqSingleton	data()[134]	4.382s	passed
getOfSeqSingletonConcrete	data()[135]	4.372s	passed
getOfSeqConcat	data()[136]	4.438s	passed
getOfSeqSub	data()[137]	4.461s	passed
getOfSeqReverse	data()[138]	4.295s	passed
lenOfSeqEmpty	data()[139]	4.334s	passed
div_unique2	data()[13]	4.430s	passed
lenOfSeqSingleton	data()[140]	4.333s	passed
lenOfSeqConcat	data()[141]	4.380s	passed
lenOfSeqSub	data()[142]	4.395s	passed
lenOfSeqReverse	data()[143]	4.341s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	4.337s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	4.377s	passed
getOfSeqSingletonEQ	data()[146]	4.383s	passed
getOfSeqConcatEQ	data()[147]	4.397s	passed
getOfSeqSubEQ	data()[148]	4.384s	passed
getOfSeqReverseEQ	data()[149]	4.399s	passed
div_exists	data()[14]	4.663s	passed
lenOfSeqEmptyEQ	data()[150]	4.435s	passed
lenOfSeqSingletonEQ	data()[151]	4.511s	passed
lenOfSeqConcatEQ	data()[152]	4.426s	passed
lenOfSeqSubEQ	data()[153]	4.487s	passed
lenOfSeqReverseEQ	data()[154]	4.460s	passed
getOfSeqDefEQ	data()[155]	4.318s	passed
lenOfSeqDefEQ	data()[156]	4.368s	passed
seqConcatWithSeqEmpty1	data()[157]	4.338s	passed
seqConcatWithSeqEmpty2	data()[158]	4.440s	passed
seqReverseOfSeqEmpty	data()[159]	4.454s	passed
div_one	data()[15]	4.429s	passed
subSeqComplete	data()[160]	4.337s	passed
subSeqTailR	data()[161]	4.446s	passed
subSeqTailL	data()[162]	4.408s	passed
subSeqTailEQR	data()[163]	4.433s	passed
subSeqTailEQL	data()[164]	4.396s	passed
seqDef_split	data()[165]	4.397s	passed
seqDef_induction_upper	data()[166]	4.433s	passed
seqDef_induction_upper_concrete	data()[167]	4.473s	passed
seqDef_induction_lower	data()[168]	4.331s	passed
seqDef_induction_lower_concrete	data()[169]	4.364s	passed
jdiv_one	data()[16]	4.286s	passed
seqDef_split_in_three	data()[170]	4.508s	passed
seqDef_empty	data()[171]	4.399s	passed
seqDef_one_summand	data()[172]	4.467s	passed
seqDef_lower_equals_upper	data()[173]	4.384s	passed
seqDefOfSeq	data()[174]	4.420s	passed
seqSelfDefinitionEQ2	data()[175]	4.310s	passed
indexOfSeqSingleton	data()[176]	4.201s	passed
indexOfSeqConcatFirst	data()[177]	4.265s	passed
indexOfSeqConcatSecond	data()[178]	4.274s	passed
indexOfSeqSub	data()[179]	4.422s	passed
div_zero	data()[17]	4.240s	passed
lenOfArray2seq	data()[180]	4.239s	passed
getAnyOfArray2seq	data()[181]	4.359s	passed
getOfArray2seq	data()[182]	4.393s	passed
getAnyOfNPermInv	data()[183]	4.310s	passed
seqNPermRange	data()[184]	4.415s	passed
seqPermTrans	data()[185]	4.457s	passed
seqPermRefl	data()[186]	4.381s	passed
seqPermSplit	data()[187]	4.418s	passed
seqNPermRight	data()[188]	4.575s	passed
seqPermFromSwap	data()[189]	4.462s	passed
divResZero1	data()[18]	4.304s	passed
seqPermTransAlt0	data()[190]	4.353s	passed
seqPermTransAlt1	data()[191]	4.221s	passed
seqPermTransAlt2	data()[192]	4.432s	passed
seqPermTransAlt3	data()[193]	4.413s	passed
seqPermForall	data()[194]	4.503s	passed
seqPermExists	data()[195]	4.575s	passed
schiffl_lemma_2	data()[196]	32.475s	passed
schiffl_thm_1	data()[197]	5.351s	passed
eqSameSeq	data()[198]	4.637s	passed
divResZero2	data()[19]	4.329s	passed
eqTermCut	data()[1]	5.381s	passed
divResOne1	data()[20]	4.352s	passed
divResOne2	data()[21]	4.495s	passed
div_cancel1	data()[22]	4.317s	passed
div_cancel2	data()[23]	4.128s	passed
divAddMultDenom	data()[24]	4.241s	passed
divMinus	data()[25]	4.260s	passed
divMinusDenom	data()[26]	4.320s	passed
divLeastDPos	data()[27]	4.158s	passed
divLeastDNeg	data()[28]	4.272s	passed
divGreatestDPos	data()[29]	4.231s	passed
equivAllRight	data()[2]	5.083s	passed
divGreatestDNeg	data()[30]	4.252s	passed
divIncreasingPos	data()[31]	4.303s	passed
divIncreasingNeg	data()[32]	4.368s	passed
jdiv_zero	data()[33]	4.288s	passed
jdivPulloutMinusNum	data()[34]	4.314s	passed
jdivPulloutMinusDenom	data()[35]	4.269s	passed
jdiv_uniquePosPos	data()[36]	4.315s	passed
jdiv_uniquePosNeg	data()[37]	4.115s	passed
jdiv_uniqueNegPos	data()[38]	4.067s	passed
jdiv_uniqueNegNeg	data()[39]	4.121s	passed
irrflConcrete1	data()[3]	4.745s	passed
jdivMultDenom1	data()[40]	4.276s	passed
jdivMultDenom2	data()[41]	4.560s	passed
mod_geZero	data()[42]	4.636s	passed
mod_lessDenom	data()[43]	4.330s	passed
jmod_NumPos	data()[44]	4.140s	passed
jmod_NumNeg	data()[45]	4.211s	passed
jmod_geZero	data()[46]	4.151s	passed
jmodNumZero	data()[47]	4.107s	passed
jmod_pulloutminusNum	data()[48]	4.169s	passed
jmod_pulloutminusDenom	data()[49]	4.048s	passed
irrflConcrete2	data()[4]	4.552s	passed
jmodUnique1	data()[50]	4.293s	passed
jmodUnique2	data()[51]	4.328s	passed
intDivRem	data()[52]	4.206s	passed
jmodjmod	data()[53]	4.332s	passed
jmodDivisible	data()[54]	4.349s	passed
jmodDivisibleRep	data()[55]	4.262s	passed
jdivAddMultDenom	data()[56]	4.569s	passed
jmodAltZero	data()[57]	4.327s	passed
jmodAddMultDenomZero	data()[58]	4.282s	passed
polyDiv_zero	data()[59]	4.174s	passed
cancel_gtPos	data()[5]	4.590s	passed
polyMod_ltdivDenom	data()[60]	4.349s	passed
bsum_empty	data()[61]	4.271s	passed
bsum_induction_upper	data()[62]	4.263s	passed
bsum_induction_lower	data()[63]	4.404s	passed
bsum_num_of_bounds	data()[64]	4.338s	passed
bsum_num_of_bounds2	data()[65]	4.310s	passed
bsum_induction_upper2	data()[66]	4.330s	passed
bsum_induction_upper_concrete	data()[67]	4.350s	passed
bsum_induction_upper_concrete_2	data()[68]	4.185s	passed
bsum_induction_upper2_concrete	data()[69]	4.212s	passed
cancel_gtNeg	data()[6]	4.683s	passed
bsum_induction_lower_concrete	data()[70]	4.221s	passed
bsum_induction_lower2	data()[71]	4.161s	passed
bsum_induction_lower2_concrete	data()[72]	4.127s	passed
bsum_positive	data()[73]	4.178s	passed
bsum_upper_bound	data()[74]	4.310s	passed
bsum_lower_bound	data()[75]	4.681s	passed
bsum_positive_lower_bound_element	data()[76]	4.286s	passed
bsum_sub_same_index	data()[77]	4.196s	passed
bsum_less_same_index	data()[78]	4.129s	passed
bsum_equal_except_one_index	data()[79]	4.134s	passed
moduloIntIsInInt	data()[7]	4.412s	passed
bsum_num_of_is_max	data()[80]	4.047s	passed
bsum_num_of_is_max2	data()[81]	4.193s	passed
bsum_num_of_is_max3	data()[82]	4.159s	passed
bsum_num_of_is_max4	data()[83]	4.200s	passed
bsum_num_of_lt_max	data()[84]	4.172s	passed
bsum_num_of_lt_max2	data()[85]	4.241s	passed
bsum_num_of_lt_max3	data()[86]	4.107s	passed
bsum_num_of_lt_max4	data()[87]	3.937s	passed
bsum_num_of_gt0	data()[88]	4.066s	passed
bsum_num_of_gt0_alt	data()[89]	3.992s	passed
moduloLongIsInLong	data()[8]	4.405s	passed
bsum_add_concrete	data()[90]	4.065s	passed
bprod_all_positive	data()[91]	4.155s	passed
bprod_split	data()[92]	4.079s	passed
powConcrete0	data()[93]	4.086s	passed
powConcrete1	data()[94]	4.030s	passed
powSplitFactor	data()[95]	4.316s	passed
powAdd	data()[96]	4.343s	passed
powMono	data()[97]	4.233s	passed
powMonoConcrete	data()[98]	4.370s	passed
powMonoConcreteRight	data()[99]	4.347s	passed
moduloShortIsInShort	data()[9]	4.345s	passed
Standard output

943        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
981        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 17.47ms 
1316       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1337       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)

2586       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2589       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2590       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2591       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4639       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
12606      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 11.29s 
12709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
12762      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.2ns 
12781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
12781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.7ns 
12788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.07s 
16860      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
18115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
18150      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.92ms 
18168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
18170      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.61ms 
18172      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21906      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 
21907      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
23212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
23247      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.56ms 
23252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
23252      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.7ns 
23258      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
26846      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
27985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
27994      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
27998      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
27998      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.4ns 
28000      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31437      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
31438      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
32540      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
32547      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
32551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
32552      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 532.1ns 
32554      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35937      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
35938      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
37082      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
37139      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.24ms 
37144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
37144      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.7ns 
37146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40670      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
40670      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
41793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
41823      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.36ms 
41828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
41829      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.1ns 
41830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45159      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
45159      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
46229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
46237      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
46240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
46240      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.2ns 
46242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49552      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
49553      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
50638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
50642      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 930.6ns 
50646      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
50646      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420.6ns 
50647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
53929      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
54985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
54989      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 767.5ns 
54992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
54992      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.7ns 
54994      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
58339      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
59421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
59425      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.7ns 
59429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
59434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.52ms 
59436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62795      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
62796      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
63874      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
63877      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851ns 
63879      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
63880      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.8ns 
63881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67136      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
67136      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
68266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
68416      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 145.47ms 
68433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
68433      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 671.3ns 
68443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
71771      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
72799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
72856      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.93ms 
72865      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
72865      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.8ns 
72872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76147      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
76148      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
77209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
77520      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 297ms 
77526      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
77526      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 478.8ns 
77528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80867      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
80867      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
81943      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
81952      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
81960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
81961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 838.7ns 
81963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
85175      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
86239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
86243      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
86248      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
86248      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.3ns 
86250      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89377      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
89378      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
90412      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
90485      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.27ms 
90490      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
90490      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 437.2ns 
90491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93749      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
93749      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
94765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
94792      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ms 
94795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
94796      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 464.2ns 
94797      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98005      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
98005      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
99095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
99120      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.38ms 
99125      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
99126      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 960.61ns 
99132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
102395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
103449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
103472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.57ms 
103475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
103476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.3ns 
103477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
106847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
107945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
107967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.31ms 
107970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
107970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.1ns 
107971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
111233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
112250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
112284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.62ms 
112287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
112287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.1ns 
112288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
115396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
116409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
116413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
116415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
116415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.2ns 
116417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
119543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
120566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
120654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.33ms 
120656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
120657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.4ns 
120658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
123802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
124811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
124913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.22ms 
124916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
124917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.6ns 
124918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
128059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
129162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
129234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.52ms 
129236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
129236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.9ns 
129237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
132345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
133379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
133392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.04ms 
133395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
133396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.01ms 
133397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
136628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
137644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
137664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.42ms 
137666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
137666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.5ns 
137667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
140850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
141880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
141895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.47ms 
141896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
141896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
141897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
145088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
146136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
146147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.94ms 
146150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
146150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.4ns 
146153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
149387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
150438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
150449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.65ms 
150452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
150453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.8ns 
150454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
153741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
154807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
154818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.05ms 
154820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
154820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.2ns 
154822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
158077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
159101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
159106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
159108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
159108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
159109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
162349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
163395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
163412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
163421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
163422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.9ns 
163424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
166605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
167612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
167688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.43ms 
167691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
167691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.9ns 
167692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
170936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
171979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
172005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.04ms 
172006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
172006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
172007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
175105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
176094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
176120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.32ms 
176121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
176121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.4ns 
176122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
179165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
180161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
180186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.49ms 
180188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
180188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
180188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
183264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
184282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
184307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.19ms 
184309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
184309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
184310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
187436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
188517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
188582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.9ms 
188593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
188593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.9ns 
188596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
192026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
193145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
193149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
193150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
193151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
193151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
196646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
197777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
197785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.44ms 
197786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
197787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
197787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
201079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
202103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
202115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
202118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
202118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.9ns 
202119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
205243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
206244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
206256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.76ms 
206258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
206258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.8ns 
206259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
209415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
210437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
210467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.81ms 
210469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
210469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
210470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
213614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
214606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
214619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.44ms 
214620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
214620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
214621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
217699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
218720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
218725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
218728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
218728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.7ns 
218729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
221878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
222888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
222894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
222896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
222896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
222897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
225954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
226925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
226942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.63ms 
226943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
226944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
226945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
230073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
231098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
231233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 125.24ms 
231238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
231239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.6ns 
231240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
234402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
235425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
235558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 123.02ms 
235569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
235569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.4ns 
235570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
238748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
239768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
239773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
239776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
239776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.61ns 
239777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
242994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
244042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
244103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.16ms 
244107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
244107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 562ns 
244109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
247371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
248405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
248454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.11ms 
248456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
248456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
248457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
251681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
252710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
252716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
252718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
252718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
252719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
256012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
257037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
257285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 233.85ms 
257287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
257287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
257288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
260560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
261592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
261612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.85ms 
261614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
261614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.4ns 
261618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
264867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
265883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
265894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.41ms 
265896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
265896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
265897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
269041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
270042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
270068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.73ms 
270070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
270070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.6ns 
270071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
273384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
274397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
274417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.65ms 
274419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
274419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
274420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
277629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
278681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
278687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
278690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
278690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
278691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
281886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
282945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
282952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
282953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
282953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
282954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
286249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
287317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
287355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.75ms 
287356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
287356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
287357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
290631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
291667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
291693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.02ms 
291696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
291696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.4ns 
291697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
294912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
295978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
296002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.62ms 
296005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
296005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.6ns 
296006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
299262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
300327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
300332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
300334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
300334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
300335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
303627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
304676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
304683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
304684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
304684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
304685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
307837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
308860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
308868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
308869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
308869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
308870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
312031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
313076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
313080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
313082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
313082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
313083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
316239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
317298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
317301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 966.4ns 
317303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
317303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
317304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
320460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
321457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
321462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
321464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
321464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
321465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
324584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
325586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
325589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
325591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
325591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.7ns 
325592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
328705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
329696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
329767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.9ms 
329770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
329770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.8ns 
329771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
332969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
334018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
334077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.92ms 
334080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
334080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.2ns 
334081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 
337662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
338706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
338758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.53ms 
338759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
338759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
338760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
341935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
342961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
343044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.65ms 
343046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
343046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
343047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
346203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
347195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
347240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.04ms 
347242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
347242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
347243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
350312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
351290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
351369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.33ms 
351372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
351372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.4ns 
351373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
354468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
355455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
355502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.71ms 
355505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
355505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.2ns 
355506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
358568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
359521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
359551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.27ms 
359552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
359552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
359553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
362673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
363706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
363743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.85ms 
363745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
363747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.38ms 
363749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
366849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
367864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
367902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.91ms 
367904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
367904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
367905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
371061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
372058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
372102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.05ms 
372104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
372104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
372105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
375201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
376237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
376274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.61ms 
376276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
376276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
376277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
379425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
380477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
380515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.62ms 
380517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
380517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
380518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
383654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
384587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
384622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.47ms 
384624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
384624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.3ns 
384625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
387571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
388528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
388559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.41ms 
388561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
388561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
388561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
391598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
392579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
392625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.39ms 
392627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
392627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
392628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
395644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
396578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
396617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.24ms 
396620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
396620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.3ns 
396621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
399668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
400671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
400682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.69ms 
400684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
400685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.6ns 
400686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
403790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
404811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
404837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.21ms 
404840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
404840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.2ns 
404841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
407957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
408911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
408916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
408917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
408917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
408918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
412032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
412999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
413003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 963.3ns 
413004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
413004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
413005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
416053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
417029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
417032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 993.8ns 
417034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
417034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
417035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
420295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
421337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
421348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.99ms 
421350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
421350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
421352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
424647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
425682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
425691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.68ms 
425694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
425694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.3ns 
425695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
428869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
429906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
429924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.06ms 
429926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
429926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
429927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
433226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
434289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
434294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
434296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
434296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
434297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
437628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
438639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
438642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 849.1ns 
438643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
438644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
438644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
441898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
442934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
442942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.37ms 
442943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
442943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
442944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
446238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
447263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
447265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 842.71ns 
447267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
447267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
447268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
450513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
451578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
451581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 998.61ns 
451582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
451582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
451583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
454836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
455887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
455890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 828.2ns 
455893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
455893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236ns 
455894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
459161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
460269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
460274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
460276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
460276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
460277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
463518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
464595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
464609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.14ms 
464611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
464611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
464612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
467856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
468895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
468901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.41ms 
468903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
468903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
468904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
472098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
473125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
473136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.82ms 
473138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
473139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.3ns 
473140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
476400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
477425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
477435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.29ms 
477436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
477436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
477437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
480672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
481714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
481739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.86ms 
481740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
481740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
481741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
484956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
485977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
485982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
485983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
485983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
485984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
489218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
490241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
490245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
490246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
490246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
490247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
493496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
494579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
494585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 
494587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
494587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.4ns 
494588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
497978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
499035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
499063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.73ms 
499066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
499066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.5ns 
499067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
502352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
503402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
503407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 737.3ns 
503410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
503410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
503411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
506645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
507692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
507752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.9ms 
507754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
507754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
507755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
511048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
512108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
512113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
512114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
512115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
512116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
515402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
516466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
516498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.79ms 
516500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
516501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.2ns 
516502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
519794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
520844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
520875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.59ms 
520880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
520880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.8ns 
520881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
524169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
525236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
525271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31ms 
525273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
525273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
525275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
528564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
529646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
529649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 882.1ns 
529651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
529651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
529652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
533007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
534081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
534088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
534090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
534091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
534091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
537429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
538515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
538519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
538521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
538521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
538522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
541845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
542918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
542922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
542923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
542923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
542924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
546274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
547366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
547369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
547370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
547371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
547371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
550695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
551775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
551780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
551783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
551783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
551784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
555147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
556245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
556250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
556257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
556257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.3ns 
556259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
559546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
560618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
560632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.14ms 
560633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
560634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
560634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
563940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
565029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
565047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.81ms 
565053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
565053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
565053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
568356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
569435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
569450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.93ms 
569452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
569452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
569453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
572721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
573821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
573842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.18ms 
573843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
573844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.1ns 
573845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
577147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
578241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
578248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
578250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
578250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.2ns 
578251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
581530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
582622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
582632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.57ms 
582633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
582633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.1ns 
582634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
585929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
587062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
587065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
587067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
587067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
587068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
590349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
591443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
591447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
591449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
591449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
591450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
594742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
595815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
595819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
595821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
595821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.7ns 
595822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
599124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
600233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
600254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.86ms 
600260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
600260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113ns 
600261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
603615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
604713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
604718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
604720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
604720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
604721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
607924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
609004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
609013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.72ms 
609015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
609016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.6ns 
609016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
612296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
613344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
613347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 980.8ns 
613349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
613349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
613350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
616597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
617677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
617680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
617681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
617682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
617682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
620977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
622055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
622060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
622062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
622062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.5ns 
622062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
625377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
626452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
626456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
626457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
626457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
626458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
629713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
630792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
630796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
630798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
630798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
630799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
634054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
635129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
635133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
635134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
635135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
635135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
638404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
639502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
639510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.73ms 
639511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
639512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
639515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
642806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
643889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
643893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
643895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
643895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
643895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
647201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
648274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
648290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.06ms 
648291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
648291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
648292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
651586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
652672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
652675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 951.8ns 
652676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
652676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
652677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
656000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
657063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
657073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.44ms 
657075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
657075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
657076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
660386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
661505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
661508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
661509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
661509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
661510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
664899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
666016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
666019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
666020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
666021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.07ms 
666022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
669337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
670436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
670445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.75ms 
670448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
670448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.5ns 
670449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
673821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
674925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
674932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
674933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
674934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
674934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
678257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
679387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
679392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
679394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
679394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
679394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
682638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
683703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
683708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
683711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
683711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
683712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
687013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
688071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
688078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
688083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
688083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.6ns 
688084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
691302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
692399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
692420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.85ms 
692421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
692421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
692422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
695742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
696835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
696859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.35ms 
696861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
696861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.3ns 
696862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
700193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
701300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
701314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.77ms 
701315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
701315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
701316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
704568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
705627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
705650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.42ms 
705652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
705652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
705653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
709006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
710057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
710096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.54ms 
710099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
710099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.8ns 
710100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
713399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
714467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
714504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.61ms 
714505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
714505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
714506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
717804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
718898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
718937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.71ms 
718939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
718939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
718940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
722221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
723313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
723333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.62ms 
723335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
723335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
723336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
726594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
727683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
727730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.52ms 
727732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
727732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
727733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
731025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
732092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
732162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.27ms 
732164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
732164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
732165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
735476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
736578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
736636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.41ms 
736638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
736638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
736638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
739852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
740906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
740967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.63ms 
740969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
740969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
740970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
744179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
745268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
745331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.87ms 
745333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
745333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
745334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
748592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
749665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
749839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 164.99ms 
749841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
749841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
749841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
753147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
754226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
754238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
754240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
754240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
754241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
757582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
757582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
758691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
758705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.14ms 
758707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
758707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
758708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
761946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
763081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
763089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
763091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
763091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
763091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
766397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
767483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
767509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.76ms 
767511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
767511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
767512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
770716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
771805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
771820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.29ms 
771821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
771821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
771822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
774947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
776016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
776020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
776022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
776022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
776023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
779210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
780259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
780285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.53ms 
780287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
780287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
780287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
783469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
784533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
784559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.89ms 
784560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
784561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
784561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
787844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
787845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
788952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
788981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.91ms 
788983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
788983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
788983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
792140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
793216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
793220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
793222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
793222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
793223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
796513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
796513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
797574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
797579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
797580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
797581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
797581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
800885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
800885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
801963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
801972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.84ms 
801973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
801973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
801974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
805217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
806273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
806282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.69ms 
806283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
806283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
806285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
809520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
809521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
810591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
810697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 98.58ms 
810698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
810698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
810699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
814008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
814008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
815109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
815154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.95ms 
815156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
815156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.2ns 
815157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
818435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
818435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
819503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
819535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.37ms 
819537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
819537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
819538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
822849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
822849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
823950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
823953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.3ns 
823955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
823955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
823956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
827165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
827166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
828232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
828528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 282.42ms 
828531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
828532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.4ns 
828533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
831830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
831830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
832919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
832991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.4ms 
832993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
832993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
832994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
836285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
836285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
837342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
837345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 661.7ns 
837346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
837346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
837347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
840499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
840500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
841562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
841565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.9ns 
841567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
841567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
841568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
844873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
845992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
845995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.2ns 
845999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
845999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.2ns 
846000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
849308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
849308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
850408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
850411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 786.8ns 
850412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
850412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
850413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
853680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
853680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
854788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
854891     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
854912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 121.57ms 
854915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
854915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.2ns 
854917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
858323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
858323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
859414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
859487     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
859488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.29ms 
859489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
859489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
859495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
862789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
862789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
863891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
863893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 
863932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
864022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
864062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
864073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
864084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
864088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
864090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
864094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
864100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
864103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
864109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
864114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
864374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
864376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
864377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
864378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
864379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
864528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
864529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
864530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
864532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
864533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
864534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
864730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
864732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
864733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
864734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
864735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
864736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
864931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
864933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
864934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
864935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
864937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
864938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
864946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
864948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
864949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
864951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
864952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
864953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
864961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
864963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
864964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
864965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
864966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
864967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
865141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
865143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
865146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
865321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
865323     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)'' 
865326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
865327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
865328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
865329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
865331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
865332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
865339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
865341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
865342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
865344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
865345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
865492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
865497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
865499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
865500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
865501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
865502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
865503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
865662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
865664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
865666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
865668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
865669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
865670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
865671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
865672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
865791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
865793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
865921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
865927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
865933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
865935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
865936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
865938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
865939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
865940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
865940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
865942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
865953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
865959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
866093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
866096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
866097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
866099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
866100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
866101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
866102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
866103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
866176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
866184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
866313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
866315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
866317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
866319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
866320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
866321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
866495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
866501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
866503     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)'' 
866505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
866506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
866507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
866508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
866516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
866528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
866532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
866533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
866534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
866706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
866709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
866710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
866711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
866712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
866713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
866857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
866859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
866860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
866862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
866863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
866864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
866865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
866866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
866982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
866984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
867087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
867088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
867089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
867095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
867101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
867107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
867265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
867267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
867268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
867270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
867283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
867397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
872255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
872257     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)'' 
872263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
872264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
872264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
872265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
872266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
872276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
872278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
872279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
872280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
872280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
872416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
872421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
872422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
872423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
872424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
872425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
872425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
872565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
872566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
872567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
872568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
872569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
872569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
872570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
872571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
872678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
872679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
872781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
872786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
872792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
872793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
872794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
872795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
872808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
872919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
872920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
872921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
872922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
873030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
873043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
873044     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)'' 
873046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
873047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
873048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
873049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
873049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
873063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
873065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
873066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
873066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
873067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
873186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
873188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
873189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
873190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
873191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
873315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
873321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
873322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
873323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
873323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
873324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
873325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
873529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
873531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
873531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
873533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
873534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
873535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
873535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
873536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
873537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
873538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
873539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
873540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
873540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
873541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
873542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
873675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
873676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
873686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
873805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
873926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
873927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
873928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
873929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
873930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
873930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
873931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
873931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
873932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
874058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
874067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
874193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
874194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
874195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
874196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
874196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
874197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
874197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
874198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
874205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
874205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
874318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
874325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
874332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
874469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
874470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
874471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
874472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
874473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
874473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
874473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
874474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
874549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
874551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
874551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
874552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
874553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
874561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
874567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
874725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
874851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
874852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
874853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
874854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
875093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
875215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
875216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
880268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
880274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
880275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
880276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
880276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
880518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
880520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
880522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
880522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
880523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
880743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
885483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
890167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
890172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
890173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
890174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
890175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
890349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
890351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
890352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
890353     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)' ...' 
890355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
891965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
891965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
891966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
895281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
895281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
896373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
896375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
896376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
896387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
896401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
896404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
896405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
896406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
896411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
896413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
896417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
896420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
896421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
896434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
896436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
896437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
896500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
896501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
896502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
896503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
896503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
896599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
896600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
896601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
896602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
896603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
896608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
896609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
896610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
896611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
896612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
896613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
896723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
896724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
896725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
896726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
896728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
896728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
896853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
896855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
896855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
896856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
896857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
896858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
896859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
896859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
896861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
896861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
896862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
896863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
896863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
896864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
896865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
896866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
896866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
896867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
896869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
896872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
896917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
896919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
896985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
896987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
896988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
896990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
896991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
896992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
897047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
897050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
897052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
897054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
897055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
897056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
897057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
897113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
897117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
897121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
897245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
897316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
897317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.6ns 
897318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
900705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
900705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
901904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
901951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.63ms