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

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

Test	Method name	Duration	Result
powPositive	data()[100]	4.235s	passed
powPositiveConcrete	data()[101]	4.199s	passed
powGeq1Concrete	data()[102]	4.197s	passed
pow2InIntLower	data()[103]	4.203s	passed
pow2InIntUpper	data()[104]	4.191s	passed
logSelfConcrete	data()[105]	4.215s	passed
log1Concrete	data()[106]	4.169s	passed
logProduct	data()[107]	4.243s	passed
logTimesBaseConcrete	data()[108]	4.294s	passed
logProdIdentity	data()[109]	4.309s	passed
moduloByteIsInByte	data()[10]	4.379s	passed
logProdIdentityConcrete	data()[110]	4.277s	passed
logPowIdentity	data()[111]	4.267s	passed
logPowIdentityConcrete	data()[112]	4.342s	passed
logPositive	data()[113]	4.232s	passed
logPositiveConcrete	data()[114]	4.170s	passed
logMono	data()[115]	4.216s	passed
logMonoConcrete	data()[116]	4.063s	passed
powLogLess	data()[117]	4.147s	passed
powLogMore2	data()[118]	4.182s	passed
logLessThanPow	data()[119]	4.118s	passed
moduloCharIsInChar	data()[11]	4.295s	passed
logLessThanPowConcrete	data()[120]	4.128s	passed
logSqueeze	data()[121]	4.047s	passed
ifthenelse_equals	data()[122]	4.069s	passed
ifthenelse_equals_1	data()[123]	4.126s	passed
ifthenelse_equals_2	data()[124]	4.063s	passed
disjointWithSingleton1	data()[125]	4.125s	passed
disjointWithSingleton2	data()[126]	4.102s	passed
disjointArrayRanges	data()[127]	4.200s	passed
disjointArrayRangeAllFields1	data()[128]	4.090s	passed
disjointArrayRangeAllFields2	data()[129]	4.179s	passed
div_unique1	data()[12]	4.557s	passed
seqSelfDefinition	data()[130]	4.262s	passed
seqOutsideValue	data()[131]	4.168s	passed
castedGetAny	data()[132]	4.146s	passed
seqGetAlphaCast	data()[133]	4.100s	passed
getOfSeqSingleton	data()[134]	4.137s	passed
getOfSeqSingletonConcrete	data()[135]	4.172s	passed
getOfSeqConcat	data()[136]	4.234s	passed
getOfSeqSub	data()[137]	4.167s	passed
getOfSeqReverse	data()[138]	4.254s	passed
lenOfSeqEmpty	data()[139]	4.172s	passed
div_unique2	data()[13]	4.452s	passed
lenOfSeqSingleton	data()[140]	4.064s	passed
lenOfSeqConcat	data()[141]	4.159s	passed
lenOfSeqSub	data()[142]	4.115s	passed
lenOfSeqReverse	data()[143]	4.103s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	4.116s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	4.097s	passed
getOfSeqSingletonEQ	data()[146]	4.215s	passed
getOfSeqConcatEQ	data()[147]	4.242s	passed
getOfSeqSubEQ	data()[148]	4.315s	passed
getOfSeqReverseEQ	data()[149]	4.189s	passed
div_exists	data()[14]	4.589s	passed
lenOfSeqEmptyEQ	data()[150]	4.284s	passed
lenOfSeqSingletonEQ	data()[151]	4.290s	passed
lenOfSeqConcatEQ	data()[152]	4.180s	passed
lenOfSeqSubEQ	data()[153]	4.240s	passed
lenOfSeqReverseEQ	data()[154]	4.201s	passed
getOfSeqDefEQ	data()[155]	4.138s	passed
lenOfSeqDefEQ	data()[156]	4.151s	passed
seqConcatWithSeqEmpty1	data()[157]	4.147s	passed
seqConcatWithSeqEmpty2	data()[158]	4.194s	passed
seqReverseOfSeqEmpty	data()[159]	4.246s	passed
div_one	data()[15]	4.342s	passed
subSeqComplete	data()[160]	4.224s	passed
subSeqTailR	data()[161]	4.174s	passed
subSeqTailL	data()[162]	4.215s	passed
subSeqTailEQR	data()[163]	4.178s	passed
subSeqTailEQL	data()[164]	4.188s	passed
seqDef_split	data()[165]	4.339s	passed
seqDef_induction_upper	data()[166]	4.371s	passed
seqDef_induction_upper_concrete	data()[167]	4.318s	passed
seqDef_induction_lower	data()[168]	4.325s	passed
seqDef_induction_lower_concrete	data()[169]	4.404s	passed
jdiv_one	data()[16]	4.413s	passed
seqDef_split_in_three	data()[170]	4.601s	passed
seqDef_empty	data()[171]	4.468s	passed
seqDef_one_summand	data()[172]	4.418s	passed
seqDef_lower_equals_upper	data()[173]	4.369s	passed
seqDefOfSeq	data()[174]	4.374s	passed
seqSelfDefinitionEQ2	data()[175]	4.396s	passed
indexOfSeqSingleton	data()[176]	4.354s	passed
indexOfSeqConcatFirst	data()[177]	4.384s	passed
indexOfSeqConcatSecond	data()[178]	4.368s	passed
indexOfSeqSub	data()[179]	4.567s	passed
div_zero	data()[17]	4.423s	passed
lenOfArray2seq	data()[180]	4.407s	passed
getAnyOfArray2seq	data()[181]	4.513s	passed
getOfArray2seq	data()[182]	4.446s	passed
getAnyOfNPermInv	data()[183]	4.406s	passed
seqNPermRange	data()[184]	4.500s	passed
seqPermTrans	data()[185]	4.395s	passed
seqPermRefl	data()[186]	4.383s	passed
seqPermSplit	data()[187]	4.268s	passed
seqNPermRight	data()[188]	4.558s	passed
seqPermFromSwap	data()[189]	4.366s	passed
divResZero1	data()[18]	4.280s	passed
seqPermTransAlt0	data()[190]	4.183s	passed
seqPermTransAlt1	data()[191]	4.174s	passed
seqPermTransAlt2	data()[192]	4.229s	passed
seqPermTransAlt3	data()[193]	4.293s	passed
seqPermForall	data()[194]	4.474s	passed
seqPermExists	data()[195]	4.433s	passed
schiffl_lemma_2	data()[196]	32.096s	passed
schiffl_thm_1	data()[197]	5.466s	passed
eqSameSeq	data()[198]	4.380s	passed
divResZero2	data()[19]	4.288s	passed
eqTermCut	data()[1]	5.024s	passed
divResOne1	data()[20]	4.215s	passed
divResOne2	data()[21]	4.230s	passed
div_cancel1	data()[22]	4.375s	passed
div_cancel2	data()[23]	4.189s	passed
divAddMultDenom	data()[24]	4.222s	passed
divMinus	data()[25]	4.203s	passed
divMinusDenom	data()[26]	4.253s	passed
divLeastDPos	data()[27]	4.164s	passed
divLeastDNeg	data()[28]	4.160s	passed
divGreatestDPos	data()[29]	4.285s	passed
equivAllRight	data()[2]	4.774s	passed
divGreatestDNeg	data()[30]	4.533s	passed
divIncreasingPos	data()[31]	4.418s	passed
divIncreasingNeg	data()[32]	4.436s	passed
jdiv_zero	data()[33]	4.506s	passed
jdivPulloutMinusNum	data()[34]	4.273s	passed
jdivPulloutMinusDenom	data()[35]	4.465s	passed
jdiv_uniquePosPos	data()[36]	4.649s	passed
jdiv_uniquePosNeg	data()[37]	4.461s	passed
jdiv_uniqueNegPos	data()[38]	4.352s	passed
jdiv_uniqueNegNeg	data()[39]	4.219s	passed
irrflConcrete1	data()[3]	4.629s	passed
jdivMultDenom1	data()[40]	4.344s	passed
jdivMultDenom2	data()[41]	4.228s	passed
mod_geZero	data()[42]	4.282s	passed
mod_lessDenom	data()[43]	4.270s	passed
jmod_NumPos	data()[44]	4.212s	passed
jmod_NumNeg	data()[45]	4.314s	passed
jmod_geZero	data()[46]	4.371s	passed
jmodNumZero	data()[47]	4.302s	passed
jmod_pulloutminusNum	data()[48]	4.339s	passed
jmod_pulloutminusDenom	data()[49]	4.291s	passed
irrflConcrete2	data()[4]	4.548s	passed
jmodUnique1	data()[50]	4.358s	passed
jmodUnique2	data()[51]	4.493s	passed
intDivRem	data()[52]	4.323s	passed
jmodjmod	data()[53]	4.189s	passed
jmodDivisible	data()[54]	4.152s	passed
jmodDivisibleRep	data()[55]	4.206s	passed
jdivAddMultDenom	data()[56]	4.342s	passed
jmodAltZero	data()[57]	4.170s	passed
jmodAddMultDenomZero	data()[58]	4.262s	passed
polyDiv_zero	data()[59]	4.186s	passed
cancel_gtPos	data()[5]	4.514s	passed
polyMod_ltdivDenom	data()[60]	4.087s	passed
bsum_empty	data()[61]	4.008s	passed
bsum_induction_upper	data()[62]	4.047s	passed
bsum_induction_lower	data()[63]	4.057s	passed
bsum_num_of_bounds	data()[64]	4.075s	passed
bsum_num_of_bounds2	data()[65]	4.269s	passed
bsum_induction_upper2	data()[66]	4.063s	passed
bsum_induction_upper_concrete	data()[67]	4.174s	passed
bsum_induction_upper_concrete_2	data()[68]	4.098s	passed
bsum_induction_upper2_concrete	data()[69]	4.188s	passed
cancel_gtNeg	data()[6]	4.401s	passed
bsum_induction_lower_concrete	data()[70]	4.080s	passed
bsum_induction_lower2	data()[71]	4.063s	passed
bsum_induction_lower2_concrete	data()[72]	4.048s	passed
bsum_positive	data()[73]	4.117s	passed
bsum_upper_bound	data()[74]	4.069s	passed
bsum_lower_bound	data()[75]	4.187s	passed
bsum_positive_lower_bound_element	data()[76]	4.112s	passed
bsum_sub_same_index	data()[77]	4.020s	passed
bsum_less_same_index	data()[78]	4.087s	passed
bsum_equal_except_one_index	data()[79]	4.202s	passed
moduloIntIsInInt	data()[7]	4.382s	passed
bsum_num_of_is_max	data()[80]	4.196s	passed
bsum_num_of_is_max2	data()[81]	4.201s	passed
bsum_num_of_is_max3	data()[82]	4.167s	passed
bsum_num_of_is_max4	data()[83]	4.240s	passed
bsum_num_of_lt_max	data()[84]	4.300s	passed
bsum_num_of_lt_max2	data()[85]	4.357s	passed
bsum_num_of_lt_max3	data()[86]	4.261s	passed
bsum_num_of_lt_max4	data()[87]	4.205s	passed
bsum_num_of_gt0	data()[88]	4.150s	passed
bsum_num_of_gt0_alt	data()[89]	4.258s	passed
moduloLongIsInLong	data()[8]	4.411s	passed
bsum_add_concrete	data()[90]	4.111s	passed
bprod_all_positive	data()[91]	4.125s	passed
bprod_split	data()[92]	4.186s	passed
powConcrete0	data()[93]	4.124s	passed
powConcrete1	data()[94]	4.135s	passed
powSplitFactor	data()[95]	4.194s	passed
powAdd	data()[96]	4.140s	passed
powMono	data()[97]	4.227s	passed
powMonoConcrete	data()[98]	4.162s	passed
powMonoConcreteRight	data()[99]	4.123s	passed
moduloShortIsInShort	data()[9]	4.422s	passed
Standard output

502        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
536        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.41ms 
860        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
884        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)

2208       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2212       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2214       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2215       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3961       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11090      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.23s 
11197      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11249      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.4ns 
11272      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11279      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.85ms 
11286      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15024      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 
15028      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16281      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.5ms 
16294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16294      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.8ns 
16296      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
19881      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21063      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.81ms 
21073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21073      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 557.9ns 
21076      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24534      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
24534      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25694      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.24ms 
25700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25701      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.9ns 
25703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29100      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
29100      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30245      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
30249      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30250      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 596.61ns 
30252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33600      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
33601      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34760      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.43ms 
34765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34765      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 529.9ns 
34767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38041      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
38042      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
39120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
39162      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.54ms 
39164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
39164      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.6ns 
39165      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
42463      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
43539      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
43544      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 949.81ns 
43553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
43553      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388ns 
43555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46904      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
46905      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
47957      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
47961      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 724ns 
47964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
47965      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.1ns 
47966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51333      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
51333      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
52379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
52383      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 945.31ns 
52386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
52387      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.1ns 
52388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55669      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
55669      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
56757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
56763      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.11ns 
56767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
56767      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.3ns 
56768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60042      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
60043      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
61056      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
61060      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 933.51ns 
61061      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
61062      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.7ns 
61063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64493      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
64493      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
65562      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
65617      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.92ms 
65619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
65619      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.6ns 
65620      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
68914      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
69971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
70069      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.63ms 
70072      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
70072      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.4ns 
70075      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73275      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
73276      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
74367      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
74657      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 278.67ms 
74661      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
74662      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.7ns 
74663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77944      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
77945      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
78993      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
79001      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
79004      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
79004      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.4ns 
79006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
82291      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
83406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
83413      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
83418      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
83419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 599.4ns 
83421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86735      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
86735      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
87781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
87838      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.95ms 
87841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
87841      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.8ns 
87842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91095      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
91096      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
92096      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
92119      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.77ms 
92122      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
92122      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 418.2ns 
92124      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
95348      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
96384      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
96406      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.03ms 
96409      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
96409      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.8ns 
96410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99554      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
99555      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
100598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
100622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.57ms 
100624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
100625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.5ns 
100626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
103824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
104829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
104852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.33ms 
104855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
104855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.4ns 
104856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
108130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
109189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
109227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.48ms 
109229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
109230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.5ns 
109231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
112383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
113412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
113416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
113418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
113418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.1ns 
113419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
116558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
117574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
117637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.1ms 
117639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
117640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns 
117641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
120745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
121740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
121840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.7ms 
121843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
121844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.4ns 
121846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
125002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
126020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
126093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.56ms 
126096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
126097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.6ns 
126100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
129234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
130245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
130257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.42ms 
130261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
130262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.43ms 
130263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
133393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
134390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
134412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.98ms 
134420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
134421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.3ns 
134422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
137580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
138684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
138702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.91ms 
138706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
138706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.2ns 
138707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
142160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
143222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
143236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ms 
143240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
143240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.4ns 
143241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
146592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
147644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
147655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.33ms 
147658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
147658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.1ns 
147659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
151001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
152081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
152092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.59ms 
152095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
152095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.8ns 
152096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
155487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
156590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
156597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
156603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
156604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.7ns 
156605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
159828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
160856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
160874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.65ms 
160876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
160876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
160877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
164078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
165222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
165338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99.45ms 
165356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
165359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.26ms 
165361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
168851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
169970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
170001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.82ms 
170004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
170005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.3ns 
170006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
173380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
174432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
174463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.79ms 
174465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
174465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.4ns 
174466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
177779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
178780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
178815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.6ms 
178817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
178817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125ns 
178819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
181978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
183007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
183034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.92ms 
183035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
183035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
183036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
186215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
187308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
187375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.35ms 
187383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
187383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.8ns 
187384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
190621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
191604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
191608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
191609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
191609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
191610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
194840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
195879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
195886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
195892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
195892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.8ns 
195893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
199098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
200148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
200160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.16ms 
200161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
200162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.8ns 
200162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
203334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
204357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
204372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.69ms 
204373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
204373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
204374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
207593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
208654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
208686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.7ms 
208688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
208688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
208688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
211970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
213044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
213057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.97ms 
213058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
213059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
213060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
216306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
217353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
217357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
217362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
217362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.9ns 
217364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
220673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
221692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
221698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
221699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
221700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns 
221701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
224942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
225983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
225989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
225991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
225991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
225992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
229186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
230224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
230347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.35ms 
230350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
230350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.7ns 
230351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
233635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
234677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
234840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 149.45ms 
234843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
234843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.8ns 
234845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
238119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
239159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
239163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
239165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
239165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.6ns 
239166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
242266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
243273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
243351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.38ms 
243353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
243354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.9ns 
243355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
246442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
247455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
247504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.88ms 
247506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
247506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
247507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
250684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
251707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
251710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
251712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
251712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
251713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
254784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
255781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
256051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 257.03ms 
256054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
256055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.4ns 
256056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
259190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
260206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
260223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.92ms 
260224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
260224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
260225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
263453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
264473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
264485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.67ms 
264486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
264486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
264487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
267635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
268646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
268670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.35ms 
268672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
268672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
268673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
271734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
272734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
272755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.46ms 
272758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
272758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
272759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
275792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
276761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
276765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
276767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
276767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
276768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
279821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
280807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
280813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ms 
280814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
280814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.1ns 
280815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
283852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
284830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
284869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.65ms 
284871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
284872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.2ns 
284873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
287946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
288914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
288944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.53ms 
288945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
288946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
288946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
292161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
293187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
293213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.61ms 
293215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
293215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.4ns 
293216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
296256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
297268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
297276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
297278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
297279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.5ns 
297280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
300434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
301444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
301451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms 
301452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
301452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.9ns 
301453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
304582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
305541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
305549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.86ms 
305550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
305550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
305551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
308678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
309731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
309736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
309738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
309739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.7ns 
309740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
312791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
313812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
313815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
313819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
313819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
313820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
316894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
317875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
317880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
317882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
317882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.3ns 
317883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
320939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
321925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
321928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
321930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
321930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
321931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
324955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
325947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
326043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 90.73ms 
326047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
326047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
326048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
329088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
330055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
330114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.87ms 
330116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
330116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
330117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
333254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
334247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
334301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.78ms 
334302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
334302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
334303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
337326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
338347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
338413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.3ms 
338415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
338415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
338416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
341412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
342386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
342433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.49ms 
342435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
342435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
342436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
345462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
346440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
346520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.14ms 
346523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
346523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257ns 
346524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
349661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
350673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
350721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.04ms 
350723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
350723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
350727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
353897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
354885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
354918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.22ms 
354919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
354919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.8ns 
354920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
358071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
359080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
359119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.22ms 
359121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
359121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
359122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
362251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
363258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
363287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.66ms 
363288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
363288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
363289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
366438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
367484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
367526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.44ms 
367528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
367528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
367529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
370752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
371762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
371826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.18ms 
371828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
371828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
371829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
375086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
376142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
376183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.1ms 
376185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
376185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.2ns 
376187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
379377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
380404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
380444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.16ms 
380446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
380446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.9ns 
380447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
383577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
384615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
384649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.71ms 
384650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
384651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
384651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
387738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
388758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
388799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.52ms 
388801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
388801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.2ns 
388802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
391982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
393017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
393057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.96ms 
393059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
393059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
393060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
396159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
397157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
397168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.95ms 
397170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
397170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
397171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
400283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
401267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
401294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.08ms 
401295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
401295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
401296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
404441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
405470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
405479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
405482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
405482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.6ns 
405483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
408565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
409600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
409603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 796.11ns 
409604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
409604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
409605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
412711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
413735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
413738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
413740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
413740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
413741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
416892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
417920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
417932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.69ms 
417934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
417934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
417935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
421050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
422064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
422072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ms 
422074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
422074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
422075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
425213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
426280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
426299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.9ms 
426301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
426301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
426302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
429440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
430457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
430461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
430462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
430462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
430463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
433573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
434582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
434584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 673ns 
434586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
434586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
434587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
437729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
438807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
438819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
438821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
438821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
438822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
442010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
443015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
443018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
443020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
443020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
443021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
446160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
447213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
447215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 861.91ns 
447217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
447217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
447218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
450342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
451416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
451419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 910.01ns 
451420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
451420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
451421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
454582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
455605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
455610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
455611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
455611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
455612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
458771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
459809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
459824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.11ms 
459826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
459826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.2ns 
459827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
462966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
463988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
463993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
463995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
463995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
463996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
467173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
468226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
468237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.41ms 
468238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
468238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.9ns 
468239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
471532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
472525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
472530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
472532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
472532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
472533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
475770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
476810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
476839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.65ms 
476841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
476841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
476842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
480028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
481112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
481117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
481118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
481118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
481119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
484368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
485380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
485384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
485385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
485385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
485386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
488626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
489718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
489724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
489727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
489727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
489728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
492889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
493928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
493957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.64ms 
493959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
493959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
493960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
497121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
498122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
498127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 675.5ns 
498129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
498129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
498130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
501288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
502282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
502343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.62ms 
502344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
502344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
502345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
505417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
506402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
506407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
506409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
506409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
506410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
509511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
510488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
510554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.92ms 
510556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
510556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
510557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
513686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
514704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
514736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.67ms 
514738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
514738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.3ns 
514739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
517830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
518815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
518854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.87ms 
518856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
518856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144ns 
518857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
521975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
522979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
522982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 978.41ns 
522984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
522984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
522985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
526022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
527021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
527029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.68ms 
527032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
527032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.4ns 
527033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
530100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
531094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
531098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
531100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
531100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
531101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
534202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
535221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
535225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
535226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
535226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
535227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
538295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
539284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
539288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
539290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
539290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
539291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
542393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
543409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
543413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
543415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
543415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
543416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
546499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
547512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
547516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
547517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
547517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
547518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
550671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
551699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
551712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.62ms 
551717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
551717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.3ns 
551718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
554802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
555786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
555805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.77ms 
555807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
555807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
555808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
558913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
559964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
559982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.32ms 
559987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
559987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.1ns 
559988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
563162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
564227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
564246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.34ms 
564247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
564247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.3ns 
564248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
567375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
568407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
568414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
568416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
568416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
568417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
571530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
572552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
572561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.09ms 
572562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
572562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
572563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
575655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
576658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
576660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
576661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
576662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
576662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
579754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
580793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
580797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
580798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
580799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.8ns 
580799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
583909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
584966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
584969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
584971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
584971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
584973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
588132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
589188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
589203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.92ms 
589205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
589205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
589206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
592356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
593365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
593370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ms 
593371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
593372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
593372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
596549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
597612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
597624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.73ms 
597625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
597625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
597626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
600744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
601793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
601796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
601799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
601799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
601800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
604831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
605858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
605861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 857.29ns 
605862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
605862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
605862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
608977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
610013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
610019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
610021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
610021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.5ns 
610022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
613143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
614130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
614134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
614136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
614136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
614137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
617222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
618231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
618237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
618239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
618239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
618240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
621328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
622349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
622353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
622355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
622355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
622356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
625443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
626441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
626450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.45ms 
626452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
626452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162ns 
626453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
629611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
630661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
630665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
630667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
630667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
630667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
633837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
634889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
634907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.01ms 
634909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
634909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
634910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
638155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
639219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
639222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
639224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
639224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
639225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
642369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
643400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
643411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.45ms 
643412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
643412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
643413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
646641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
647692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
647695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
647696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
647696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
647697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
650905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
651982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
651985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
651987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
651987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
651988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
655131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
656158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
656165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
656166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
656166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
656167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
659359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
660401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
660405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
660407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
660407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
660408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
663517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
664601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
664607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
664608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
664608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
664609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
667697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
668739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
668744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms 
668746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
668746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
668747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
671861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
672888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
672895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
672897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
672897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
672898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
675993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
677019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
677042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.89ms 
677044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
677044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
677045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
680172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
681215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
681237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.31ms 
681239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
681239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
681240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
684424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
685465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
685482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.77ms 
685484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
685485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.2ns 
685486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
688637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
689690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
689707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.72ms 
689708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
689708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
689709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
692824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
693841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
693880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.43ms 
693881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
693881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
693882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
697014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
698054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
698095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.24ms 
698097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
698097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
698098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
701194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
702234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
702272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.06ms 
702275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
702275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.7ns 
702276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
705408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
706439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
706461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.35ms 
706463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
706463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
706464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
709664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
710752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
710800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.15ms 
710802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
710802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
710804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
714047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
715088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
715170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.84ms 
715173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
715174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.2ns 
715175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
718380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
719427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
719489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56ms 
719490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
719490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
719491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
722636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
723740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
723814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.45ms 
723816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
723816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
723817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
727046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
728146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
728219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.57ms 
728220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
728220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
728221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
731491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
732597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
732818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 213.02ms 
732820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
732821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.9ns 
732821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
736218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
737275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
737287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.16ms 
737289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
737289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
737289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
740619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
741693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
741705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
741706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
741707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
741707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
744952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
746066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
746075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.17ms 
746076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
746076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
746077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
749346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
750419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
750449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.73ms 
750450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
750450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.9ns 
750451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
753744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
754827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
754845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.4ms 
754846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
754846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
754847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
758099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
759193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
759199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
759200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
759200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
759201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
762489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
763555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
763582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.36ms 
763584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
763584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.8ns 
763585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
766827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
767922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
767950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.05ms 
767951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
767951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
767953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
771383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
772483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
772518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.46ms 
772519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
772519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
772520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
775835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
776919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
776923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
776926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
776926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
776927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
780321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
781430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
781437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
781438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
781439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
781440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
784796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
785874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
785884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.07ms 
785885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
785885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
785886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
789147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
790281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
790290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.25ms 
790291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
790291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
790292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
793552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
793553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
794672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
794789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.25ms 
794791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
794791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
794792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
798054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
798054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
799138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
799184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.46ms 
799187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
799187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.5ns 
799188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
802435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
802435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
803531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
803567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.05ms 
803568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
803569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
803569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
806754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
806754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
807832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
807836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.6ns 
807840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
807840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
807841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
811040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
811040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
812082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
812392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 296.38ms 
812395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
812395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.7ns 
812396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
815605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
815605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
816674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
816759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.39ms 
816761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
816761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
816762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
819898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
819899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
820940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
820942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 597.2ns 
820944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
820944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
820945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
824062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
824063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
825113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
825116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 504.5ns 
825117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
825117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
825118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
828277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
828278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
829342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
829345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.5ns 
829347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
829347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
829347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
832542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
832543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
833635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
833638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 738.8ns 
833639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
833639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
833640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
836873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
836873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
837964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
838111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 144.38ms 
838115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
838115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.7ns 
838116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
841405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
841405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
842480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
842545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.81ms 
842547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
842547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
842553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
845778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
845778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
846887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
846889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
846929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
846977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
846999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
847004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
847013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
847021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
847022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
847024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
847028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
847031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
847033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
847035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
847333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
847335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
847336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
847337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
847339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
847490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
847492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
847496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
847499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
847500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
847502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
847734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
847737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
847738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
847738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
847740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
847741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
847911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
847913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
847914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
847915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
847917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
847918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
847927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
847928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
847929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
847932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
847933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
847934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
847944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
847945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
847946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
847948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
847949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
847950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
848191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
848192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
848194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
848397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
848398     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)'' 
848402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
848403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
848405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
848406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
848407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
848408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
848414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
848415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
848417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
848418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
848419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
848608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
848615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
848616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
848617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
848618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
848623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
848624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
848846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
848848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
848849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
848851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
848852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
848853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
848854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
848856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
848985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
848987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
849140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
849146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
849152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
849153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
849154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
849156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
849157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
849157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
849158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
849160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
849170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
849176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
849307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
849309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
849310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
849311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
849312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
849313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
849314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
849315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
849399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
849406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
849546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
849548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
849551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
849552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
849553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
849554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
849739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
849746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
849747     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)'' 
849749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
849750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
849751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
849752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
849753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
849772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
849774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
849775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
849777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
849926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
849928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
849929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
849930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
849931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
849932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
850086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
850088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
850089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
850091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
850092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
850093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
850094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
850095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
850221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
850223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
850331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
850332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
850333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
850339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
850346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
850352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
850535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
850538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
850539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
850540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
850554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
850686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
855908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
855909     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)'' 
855916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
855917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
855917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
855920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
855921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
855934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
855937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
855938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
855939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
855940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
856075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
856080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
856081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
856082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
856082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
856084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
856085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
856226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
856228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
856229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
856232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
856233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
856233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
856234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
856235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
856353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
856355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
856463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
856469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
856475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
856477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
856477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
856479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
856494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
856613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
856614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
856615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
856618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
856725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
856742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
856743     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)'' 
856745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
856746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
856747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
856748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
856748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
856763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
856765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
856766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
856766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
856767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
856944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
856947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
856948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
856949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
856950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
857078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
857084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
857086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
857087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
857087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
857088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
857089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
857226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
857228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
857229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
857230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
857231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
857232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
857232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
857234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
857235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
857236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
857237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
857238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
857238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
857239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
857240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
857375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
857377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
857388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
857501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
857614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
857616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
857617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
857618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
857619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
857620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
857620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
857621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
857622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
857747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
857756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
857889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
857891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
857892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
857894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
857895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
857895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
857896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
857898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
857905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
857912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
858030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
858038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
858045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
858198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
858201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
858201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
858203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
858204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
858204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
858205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
858206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
858289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
858291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
858292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
858293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
858295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
858302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
858310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
858473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
858605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
858607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
858608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
858609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
858857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
858989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
858990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
863364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
863378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
863379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
863380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
863381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
863549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
863552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
863553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
863555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
863556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
863714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
868286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
872782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
872788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
872789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
872790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
872790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
872957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
872959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
872961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
872962     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)' ...' 
872965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
874643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
874643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.6ns 
874644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
878087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
878087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
879145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
879146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
879147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
879155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
879169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
879172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
879174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
879175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
879180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
879182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
879185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
879188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
879189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
879200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
879202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
879203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
879268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
879270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
879270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
879271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
879272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
879367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
879367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
879369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
879370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
879371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
879376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
879377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
879377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
879378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
879379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
879380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
879506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
879507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
879508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
879509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
879510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
879511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
879643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
879644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
879644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
879645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
879646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
879647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
879647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
879648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
879649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
879649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
879650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
879650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
879651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
879651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
879652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
879652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
879653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
879654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
879655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
879658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
879714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
879716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
879802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
879803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
879805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
879806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
879807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
879808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
879876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
879879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
879880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
879882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
879883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
879884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
879885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
879953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
879956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
879960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
880033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
880109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
880109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
880113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
883321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
883321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
884438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
884487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.31ms