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

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

Test	Method name	Duration	Result
powPositive	data()[100]	4.133s	passed
powPositiveConcrete	data()[101]	4.048s	passed
powGeq1Concrete	data()[102]	4.161s	passed
pow2InIntLower	data()[103]	4.198s	passed
pow2InIntUpper	data()[104]	4.178s	passed
logSelfConcrete	data()[105]	4.125s	passed
log1Concrete	data()[106]	4.201s	passed
logProduct	data()[107]	4.265s	passed
logTimesBaseConcrete	data()[108]	4.193s	passed
logProdIdentity	data()[109]	4.380s	passed
moduloByteIsInByte	data()[10]	4.498s	passed
logProdIdentityConcrete	data()[110]	4.300s	passed
logPowIdentity	data()[111]	4.341s	passed
logPowIdentityConcrete	data()[112]	4.213s	passed
logPositive	data()[113]	4.359s	passed
logPositiveConcrete	data()[114]	4.320s	passed
logMono	data()[115]	4.329s	passed
logMonoConcrete	data()[116]	4.360s	passed
powLogLess	data()[117]	4.240s	passed
powLogMore2	data()[118]	4.098s	passed
logLessThanPow	data()[119]	4.292s	passed
moduloCharIsInChar	data()[11]	4.477s	passed
logLessThanPowConcrete	data()[120]	4.283s	passed
logSqueeze	data()[121]	4.151s	passed
ifthenelse_equals	data()[122]	4.270s	passed
ifthenelse_equals_1	data()[123]	4.236s	passed
ifthenelse_equals_2	data()[124]	4.192s	passed
disjointWithSingleton1	data()[125]	4.304s	passed
disjointWithSingleton2	data()[126]	4.404s	passed
disjointArrayRanges	data()[127]	4.276s	passed
disjointArrayRangeAllFields1	data()[128]	4.148s	passed
disjointArrayRangeAllFields2	data()[129]	4.360s	passed
div_unique1	data()[12]	4.511s	passed
seqSelfDefinition	data()[130]	4.174s	passed
seqOutsideValue	data()[131]	4.289s	passed
castedGetAny	data()[132]	4.299s	passed
seqGetAlphaCast	data()[133]	4.276s	passed
getOfSeqSingleton	data()[134]	4.282s	passed
getOfSeqSingletonConcrete	data()[135]	4.334s	passed
getOfSeqConcat	data()[136]	4.036s	passed
getOfSeqSub	data()[137]	4.202s	passed
getOfSeqReverse	data()[138]	4.258s	passed
lenOfSeqEmpty	data()[139]	4.368s	passed
div_unique2	data()[13]	4.507s	passed
lenOfSeqSingleton	data()[140]	4.373s	passed
lenOfSeqConcat	data()[141]	4.265s	passed
lenOfSeqSub	data()[142]	4.161s	passed
lenOfSeqReverse	data()[143]	4.200s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	4.287s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	4.237s	passed
getOfSeqSingletonEQ	data()[146]	4.234s	passed
getOfSeqConcatEQ	data()[147]	4.183s	passed
getOfSeqSubEQ	data()[148]	4.248s	passed
getOfSeqReverseEQ	data()[149]	4.227s	passed
div_exists	data()[14]	4.661s	passed
lenOfSeqEmptyEQ	data()[150]	4.287s	passed
lenOfSeqSingletonEQ	data()[151]	4.255s	passed
lenOfSeqConcatEQ	data()[152]	4.234s	passed
lenOfSeqSubEQ	data()[153]	4.196s	passed
lenOfSeqReverseEQ	data()[154]	4.380s	passed
getOfSeqDefEQ	data()[155]	4.309s	passed
lenOfSeqDefEQ	data()[156]	4.196s	passed
seqConcatWithSeqEmpty1	data()[157]	4.137s	passed
seqConcatWithSeqEmpty2	data()[158]	4.284s	passed
seqReverseOfSeqEmpty	data()[159]	4.520s	passed
div_one	data()[15]	4.314s	passed
subSeqComplete	data()[160]	4.607s	passed
subSeqTailR	data()[161]	4.629s	passed
subSeqTailL	data()[162]	4.635s	passed
subSeqTailEQR	data()[163]	4.638s	passed
subSeqTailEQL	data()[164]	4.669s	passed
seqDef_split	data()[165]	4.681s	passed
seqDef_induction_upper	data()[166]	4.792s	passed
seqDef_induction_upper_concrete	data()[167]	4.817s	passed
seqDef_induction_lower	data()[168]	4.690s	passed
seqDef_induction_lower_concrete	data()[169]	4.703s	passed
jdiv_one	data()[16]	4.261s	passed
seqDef_split_in_three	data()[170]	4.546s	passed
seqDef_empty	data()[171]	4.236s	passed
seqDef_one_summand	data()[172]	4.262s	passed
seqDef_lower_equals_upper	data()[173]	4.308s	passed
seqDefOfSeq	data()[174]	4.355s	passed
seqSelfDefinitionEQ2	data()[175]	4.258s	passed
indexOfSeqSingleton	data()[176]	4.395s	passed
indexOfSeqConcatFirst	data()[177]	4.370s	passed
indexOfSeqConcatSecond	data()[178]	4.339s	passed
indexOfSeqSub	data()[179]	4.366s	passed
div_zero	data()[17]	4.319s	passed
lenOfArray2seq	data()[180]	4.417s	passed
getAnyOfArray2seq	data()[181]	4.359s	passed
getOfArray2seq	data()[182]	4.264s	passed
getAnyOfNPermInv	data()[183]	4.276s	passed
seqNPermRange	data()[184]	4.213s	passed
seqPermTrans	data()[185]	4.218s	passed
seqPermRefl	data()[186]	4.179s	passed
seqPermSplit	data()[187]	4.158s	passed
seqNPermRight	data()[188]	4.554s	passed
seqPermFromSwap	data()[189]	4.342s	passed
divResZero1	data()[18]	4.260s	passed
seqPermTransAlt0	data()[190]	4.350s	passed
seqPermTransAlt1	data()[191]	4.196s	passed
seqPermTransAlt2	data()[192]	4.230s	passed
seqPermTransAlt3	data()[193]	4.358s	passed
seqPermForall	data()[194]	4.560s	passed
seqPermExists	data()[195]	4.441s	passed
schiffl_lemma_2	data()[196]	29.664s	passed
schiffl_thm_1	data()[197]	5.215s	passed
eqSameSeq	data()[198]	4.509s	passed
divResZero2	data()[19]	4.310s	passed
eqTermCut	data()[1]	5.363s	passed
divResOne1	data()[20]	4.227s	passed
divResOne2	data()[21]	4.137s	passed
div_cancel1	data()[22]	4.246s	passed
div_cancel2	data()[23]	4.157s	passed
divAddMultDenom	data()[24]	4.417s	passed
divMinus	data()[25]	4.593s	passed
divMinusDenom	data()[26]	4.282s	passed
divLeastDPos	data()[27]	4.315s	passed
divLeastDNeg	data()[28]	4.279s	passed
divGreatestDPos	data()[29]	4.252s	passed
equivAllRight	data()[2]	4.529s	passed
divGreatestDNeg	data()[30]	4.159s	passed
divIncreasingPos	data()[31]	4.136s	passed
divIncreasingNeg	data()[32]	4.166s	passed
jdiv_zero	data()[33]	4.149s	passed
jdivPulloutMinusNum	data()[34]	4.256s	passed
jdivPulloutMinusDenom	data()[35]	4.398s	passed
jdiv_uniquePosPos	data()[36]	4.195s	passed
jdiv_uniquePosNeg	data()[37]	4.301s	passed
jdiv_uniqueNegPos	data()[38]	4.450s	passed
jdiv_uniqueNegNeg	data()[39]	4.353s	passed
irrflConcrete1	data()[3]	4.568s	passed
jdivMultDenom1	data()[40]	4.390s	passed
jdivMultDenom2	data()[41]	4.515s	passed
mod_geZero	data()[42]	4.378s	passed
mod_lessDenom	data()[43]	4.290s	passed
jmod_NumPos	data()[44]	4.208s	passed
jmod_NumNeg	data()[45]	4.284s	passed
jmod_geZero	data()[46]	4.273s	passed
jmodNumZero	data()[47]	4.319s	passed
jmod_pulloutminusNum	data()[48]	4.324s	passed
jmod_pulloutminusDenom	data()[49]	4.302s	passed
irrflConcrete2	data()[4]	4.472s	passed
jmodUnique1	data()[50]	4.440s	passed
jmodUnique2	data()[51]	4.437s	passed
intDivRem	data()[52]	4.254s	passed
jmodjmod	data()[53]	4.284s	passed
jmodDivisible	data()[54]	4.347s	passed
jmodDivisibleRep	data()[55]	4.324s	passed
jdivAddMultDenom	data()[56]	4.445s	passed
jmodAltZero	data()[57]	4.326s	passed
jmodAddMultDenomZero	data()[58]	4.040s	passed
polyDiv_zero	data()[59]	4.168s	passed
cancel_gtPos	data()[5]	4.485s	passed
polyMod_ltdivDenom	data()[60]	4.323s	passed
bsum_empty	data()[61]	4.159s	passed
bsum_induction_upper	data()[62]	4.329s	passed
bsum_induction_lower	data()[63]	4.365s	passed
bsum_num_of_bounds	data()[64]	4.381s	passed
bsum_num_of_bounds2	data()[65]	4.258s	passed
bsum_induction_upper2	data()[66]	4.286s	passed
bsum_induction_upper_concrete	data()[67]	4.422s	passed
bsum_induction_upper_concrete_2	data()[68]	4.318s	passed
bsum_induction_upper2_concrete	data()[69]	4.383s	passed
cancel_gtNeg	data()[6]	4.488s	passed
bsum_induction_lower_concrete	data()[70]	4.297s	passed
bsum_induction_lower2	data()[71]	4.113s	passed
bsum_induction_lower2_concrete	data()[72]	3.998s	passed
bsum_positive	data()[73]	4.300s	passed
bsum_upper_bound	data()[74]	4.253s	passed
bsum_lower_bound	data()[75]	4.340s	passed
bsum_positive_lower_bound_element	data()[76]	4.289s	passed
bsum_sub_same_index	data()[77]	4.053s	passed
bsum_less_same_index	data()[78]	4.245s	passed
bsum_equal_except_one_index	data()[79]	4.189s	passed
moduloIntIsInInt	data()[7]	4.440s	passed
bsum_num_of_is_max	data()[80]	4.086s	passed
bsum_num_of_is_max2	data()[81]	4.247s	passed
bsum_num_of_is_max3	data()[82]	4.282s	passed
bsum_num_of_is_max4	data()[83]	4.217s	passed
bsum_num_of_lt_max	data()[84]	4.391s	passed
bsum_num_of_lt_max2	data()[85]	4.262s	passed
bsum_num_of_lt_max3	data()[86]	4.271s	passed
bsum_num_of_lt_max4	data()[87]	4.231s	passed
bsum_num_of_gt0	data()[88]	4.308s	passed
bsum_num_of_gt0_alt	data()[89]	4.289s	passed
moduloLongIsInLong	data()[8]	4.360s	passed
bsum_add_concrete	data()[90]	4.210s	passed
bprod_all_positive	data()[91]	4.143s	passed
bprod_split	data()[92]	4.167s	passed
powConcrete0	data()[93]	4.229s	passed
powConcrete1	data()[94]	4.248s	passed
powSplitFactor	data()[95]	4.261s	passed
powAdd	data()[96]	4.159s	passed
powMono	data()[97]	4.295s	passed
powMonoConcrete	data()[98]	4.212s	passed
powMonoConcreteRight	data()[99]	4.161s	passed
moduloShortIsInShort	data()[9]	4.379s	passed
Standard output

599        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
629        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.25ms 
911        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
931        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)

2166       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2169       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2174       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2174       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4254       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
12046      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 11.13s 
12156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
12205      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.7ns 
12225      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
12227      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.92ms 
12232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.02s 
16258      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
17535      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
17573      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.57ms 
17589      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
17590      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.8ns 
17592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21007      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
21007      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
22097      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
22116      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms 
22119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
22120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.3ns 
22121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25553      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
25553      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
26663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
26682      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.95ms 
26687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
26687      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.2ns 
26690      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30059      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
30059      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
31141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
31156      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.18ms 
31162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
31162      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.2ns 
31166      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34531      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
34531      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
35582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
35644      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.85ms 
35648      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
35650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.05ms 
35651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39016      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
39016      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
40099      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
40132      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.85ms 
40137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
40137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.9ns 
40139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43481      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
43481      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
44568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
44574      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
44577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
44577      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.8ns 
44578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47815      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
47816      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
48929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
48934      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.3ns 
48939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
48940      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.9ns 
48941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52223      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
52224      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
53312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
53316      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.9ns 
53318      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
53319      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 511.3ns 
53320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56753      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
56753      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
57811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
57814      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 906.31ns 
57816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
57816      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
57818      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61175      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
61176      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
62287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
62290      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720.71ns 
62294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
62295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.47ms 
62297      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65532      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
65533      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
66680      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
66800      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 115.09ms 
66804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
66805      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.8ns 
66806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70155      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
70155      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
71240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
71310      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.73ms 
71312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
71312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.7ns 
71314      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74639      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
74640      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
75685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
75970      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 271.9ms 
75975      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
75976      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.2ns 
75977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79251      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
79251      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
80279      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
80286      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ms 
80289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
80289      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.9ns 
80290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83443      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
83444      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
84542      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
84547      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
84551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
84551      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.8ns 
84553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87737      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
87738      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
88805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
88868      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.73ms 
88871      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
88872      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.5ns 
88873      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92071      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
92071      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
93080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
93128      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.79ms 
93131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
93131      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
93132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96370      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
96370      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
97412      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
97438      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.33ms 
97442      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
97443      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 933.81ns 
97448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
100593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
101642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
101666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.56ms 
101669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
101669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.3ns 
101670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
104777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
105779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
105802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.39ms 
105806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
105806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.4ns 
105807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
108990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
110008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
110048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.52ms 
110052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
110052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.5ns 
110053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
113200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
114201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
114206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
114208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
114209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 739ns 
114210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
117493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
118556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
118623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.84ms 
118626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
118626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.7ns 
118627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
122068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
123125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
123215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.66ms 
123219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
123219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.2ns 
123221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
126438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
127421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
127497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.91ms 
127502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
127504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.74ms 
127506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
130744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
131801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
131814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
131816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
131816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.5ns 
131817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
135034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
136074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
136093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.77ms 
136095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
136095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.8ns 
136096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
139315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
140332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
140346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ms 
140347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
140347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.2ns 
140349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
143498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
144488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
144504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms 
144506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
144506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
144507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
147631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
148628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
148640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
148644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
148644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.3ns 
148645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
151796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
152799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
152808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.55ms 
152809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
152809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
152810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
155936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
156952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
156957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
156958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
156958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
156959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
160184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
161196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
161212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.29ms 
161214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
161214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.8ns 
161215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
164484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
165535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
165610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.79ms 
165613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
165616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.24ms 
165618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
168717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
169781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
169806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.14ms 
169808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
169808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
169809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
173029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
174078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
174107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.77ms 
174109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
174109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
174110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
177412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
178527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
178556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.15ms 
178559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
178560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.2ns 
178561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
181804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
182884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
182910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.43ms 
182911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
182911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.9ns 
182913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
186212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
187233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
187300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.91ms 
187303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
187303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332ns 
187304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
190711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
191811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
191816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
191818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
191818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.3ns 
191819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
195141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
196188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
196194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
196197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
196197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.5ns 
196198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
199456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
200472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
200484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.87ms 
200486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
200486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.7ns 
200487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
203615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
204679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
204692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.07ms 
204694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
204694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
204695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
207928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
208946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
208975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.88ms 
208978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
208978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
208980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
212206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
213237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
213249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
213251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
213251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
213252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
216443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
217559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
217564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
217575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
217576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.2ns 
217577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
220814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
221889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
221894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
221897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
221898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296ns 
221900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
225203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
226190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
226197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
226199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
226199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258ns 
226201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
229417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
230479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
230635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 146.06ms 
230642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
230643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.7ns 
230644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
233854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
234939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
235077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127.42ms 
235080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
235081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.4ns 
235082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
238254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
239328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
239332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
239334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
239335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.7ns 
239336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
242549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
243552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
243615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.55ms 
243618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
243619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 573.2ns 
243620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
246864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
247918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
247963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.2ms 
247965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
247965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
247966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
251231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
252284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
252287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
252291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
252292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 707.9ns 
252294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
255424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
256482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
256733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 227.64ms 
256735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
256735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
256736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
260008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
261000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
261059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.85ms 
261061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
261061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.8ns 
261062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
264111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
265087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
265099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.12ms 
265101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
265101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
265102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
268241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
269242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
269268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.07ms 
269269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
269269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
269270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
272469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
273569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
273589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.29ms 
273592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
273592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.3ns 
273594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
276778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
277744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
277749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
277751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
277751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
277751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
281008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
282068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
282078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.25ms 
282080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
282080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
282081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
285360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
286407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
286443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.11ms 
286445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
286445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
286446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
289731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
290796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
290823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.39ms 
290826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
290826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.5ns 
290827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
294038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
295051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
295081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.64ms 
295084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
295084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.9ns 
295085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
298314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
299364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
299368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
299370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
299370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
299371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
302681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
303782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
303789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.95ms 
303792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
303792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.9ns 
303793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
307081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
308100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
308108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms 
308110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
308110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
308111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
311424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
312486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
312491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
312493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
312494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.2ns 
312495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
315744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
316785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
316788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 993.01ns 
316792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
316792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.9ns 
316793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
319974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
320897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
320902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
320904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
320904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
320905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
323904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
324896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
324900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
324902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
324902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.1ns 
324903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
328112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
329133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
329200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.36ms 
329203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
329203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341ns 
329204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
332366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
333384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
333453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.66ms 
333455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
333455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
333456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
336704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
337736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
337793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.48ms 
337795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
337796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.6ns 
337797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
340998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
342010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
342082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.45ms 
342083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
342083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
342084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
345093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
346081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
346135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.72ms 
346137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
346137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
346138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
349272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
350294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
350380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.38ms 
350382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
350383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.5ns 
350384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
353467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
354523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
354569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.19ms 
354571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
354571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.7ns 
354571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
357641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
358622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
358655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.49ms 
358657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
358657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.1ns 
358658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
361797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
362858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
362901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.92ms 
362905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
362905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.5ns 
362906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
366150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
367155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
367184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.62ms 
367186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
367186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
367187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
370326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
371360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
371401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.34ms 
371402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
371403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.5ns 
371404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
374717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
375752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
375793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.07ms 
375794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
375794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
375795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
379002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
380009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
380054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.65ms 
380057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
380057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.8ns 
380058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
383263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
384285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
384325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.65ms 
384327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
384327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
384328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
387446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
388515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
388557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.62ms 
388558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
388558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
388559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
391783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
392827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
392864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.55ms 
392866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
392866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
392866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
396094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
397114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
397153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.51ms 
397154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
397155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
397155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
400317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
401350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
401363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.41ms 
401365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
401365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
401366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
404479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
405478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
405506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.36ms 
405508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
405508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
405509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
408610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
409668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
409673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
409675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
409675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
409676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
412879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
413897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
413901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
413904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
413905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.1ns 
413906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
417096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
418146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
418150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
418152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
418152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.9ns 
418153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
421411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
422399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
422411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.79ms 
422412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
422412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
422413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
425542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
426562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
426571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.46ms 
426572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
426572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.8ns 
426573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
429806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
430843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
430865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.7ms 
430867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
430867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.9ns 
430868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
434041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
435073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
435077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
435079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
435079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
435079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
438254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
439236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
439238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 681.91ns 
439240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
439240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
439241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
442361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
443353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
443371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.39ms 
443374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
443375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.38ms 
443376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
446424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
447417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
447419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 887.71ns 
447421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
447421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
447422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
450564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
451577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
451580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 862.81ns 
451582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
451582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
451583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
454771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
455775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
455778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 805.61ns 
455779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
455779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
455780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
458934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
459951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
459956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
459958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
459958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
459958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
463047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
464069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
464081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.04ms 
464083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
464083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
464084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
467243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
468277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
468282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
468284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
468284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
468285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
471534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
472538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
472548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.74ms 
472549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
472549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
472550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
475739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
476734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
476740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
476742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
476742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
476742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
480024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
481090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
481120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.23ms 
481124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
481125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
481125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
484319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
485418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
485423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
485424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
485424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
485425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
488703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
489758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
489763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
489764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
489765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
489765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
492933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
493971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
493976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 
493978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
493978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
493979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
497220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
498303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
498335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.06ms 
498338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
498339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.35ms 
498340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
501571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
502647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
502653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.51ns 
502656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
502656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
502658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
505921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
506926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
506984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.09ms 
506986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
506986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
506987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
510292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
511339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
511344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
511347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
511347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.5ns 
511348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
514526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
515554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
515585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.56ms 
515587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
515587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
515588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
518693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
519652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
519684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.5ms 
519685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
519685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
519686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
522893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
523937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
523975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.91ms 
523976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
523976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
523977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
527176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
528255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
528258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717.8ns 
528262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
528262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.4ns 
528263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
531416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
532402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
532410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.71ms 
532412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
532412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
532412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
535623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
536675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
536680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
536682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
536682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
536683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
539845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
540913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
540917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
540918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
540918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
540919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
544101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
545104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
545108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
545109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
545109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
545110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
548343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
549408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
549413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
549414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
549414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
549415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
552781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
553812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
553816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
553818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
553818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
553819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
557069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
558078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
558092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.92ms 
558094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
558094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
558094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
561197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
562223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
562240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.63ms 
562241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
562241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
562242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
565501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
566583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
566600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms 
566601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
566602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
566603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
569728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
570754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
570774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.3ms 
570776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
570776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.3ns 
570777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
573989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
575057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
575063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
575065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
575065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
575065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
578269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
579348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
579362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.52ms 
579364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
579364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
579365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
582608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
583636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
583639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 803.31ns 
583640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
583640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
583640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
586843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
587916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
587920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
587922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
587922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
587924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
591201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
592251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
592254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
592255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
592255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
592256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
595210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
596271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
596290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.72ms 
596292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
596292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
596293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
599470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
600485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
600492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.37ms 
600493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
600494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
600494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
603680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
604740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
604750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.99ms 
604752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
604752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.9ns 
604753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
608032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
609116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
609119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 969.21ns 
609120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
609120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
609121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
612399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
613488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
613491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 842.41ns 
613493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
613493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
613493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
616673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
617751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
617757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
617758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
617758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
617759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
620896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
621913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
621918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
621919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
621919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
621920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
625073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
626113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
626118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
626119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
626119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
626120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
629354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
630400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
630404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
630405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
630406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
630406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
633577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
634634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
634641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.36ms 
634643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
634643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
634644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
637816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
638871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
638875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
638876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
638876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
638877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
642048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
643041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
643058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.83ms 
643059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
643059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
643060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
646261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
647294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
647307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.68ms 
647308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
647308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
647309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
650478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
651523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
651533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.77ms 
651535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
651535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
651536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
654751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
655817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
655821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
655822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
655822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
655823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
659039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
660073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
660076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
660077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
660077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
660078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
663245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
664302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
664309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
664311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
664311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
664312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
667459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
668501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
668506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
668507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
668507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
668508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
671770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
672880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
672885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
672887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
672887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
672888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
676089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
677189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
677194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
677196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
677196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
677197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
680333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
681384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
681390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
681392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
681392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
681393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
684434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
685507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
685528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.05ms 
685529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
685529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
685530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
688743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
689788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
689811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.64ms 
689813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
689813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
689814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
693175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
694318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
694332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.29ms 
694333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
694333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
694334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
697762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
698921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
698938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ms 
698939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
698939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
698940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
702380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
703526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
703567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.81ms 
703569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
703569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
703570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
707022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
708166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
708202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.57ms 
708204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
708204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
708205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
711643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
712801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
712840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.97ms 
712842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
712842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
712843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
716328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
717485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
717509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.73ms 
717510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
717510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
717511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
720977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
722140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
722190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.96ms 
722191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
722191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
722192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
725706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
726902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
726982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.9ms 
726984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
726984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126ns 
726985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
730550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
731737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
731799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.95ms 
731801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
731801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
731802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
735295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
736430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
736489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.71ms 
736491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
736491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107ns 
736492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
739983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
741125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
741191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.45ms 
741194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
741194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
741195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
744489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
745566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
745737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 161.67ms 
745739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
745739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
745740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
748900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
749960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
749974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.65ms 
749976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
749976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
749977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
753161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
754225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
754236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.75ms 
754237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
754237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
754238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
757469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
757469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
758537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
758544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
758546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
758546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
758547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
761777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
762872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
762899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.62ms 
762901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
762901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
762901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
766078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
767140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
767157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.03ms 
767159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
767159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
767160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
770417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
771548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
771553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
771554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
771554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
771555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
774835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
775898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
775923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.32ms 
775924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
775925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
775925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
779164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
780238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
780261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.95ms 
780263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
780263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
780264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
783495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
784598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
784627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.05ms 
784629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
784629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
784630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
787888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
787888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
789041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
789044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
789046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
789046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.1ns 
789047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
792301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
793398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
793403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
793405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
793405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
793406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
796611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
796611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
797659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
797667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.87ms 
797669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
797669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
797670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
800922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
800922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
801935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
801944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.53ms 
801945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
801945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
801946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
805066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
806054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
806156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.76ms 
806157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
806158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.6ns 
806159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
809309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
809309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
810332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
810374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.28ms 
810376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
810376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229ns 
810377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
813460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
813460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
814523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
814553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.53ms 
814555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
814555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
814556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
817672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
817672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
818709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
818712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 367.3ns 
818713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
818713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
818714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
821881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
821881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
822923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
823265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 329.03ms 
823267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
823268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.8ns 
823269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
826437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
826437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
827529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
827607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.61ms 
827609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
827609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
827610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
830903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
830904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
831955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
831957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 478.3ns 
831959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
831959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
831960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
835091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
835091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
836150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
836153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 724.21ns 
836155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
836155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
836156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
839292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
839292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
840380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
840383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 479.7ns 
840385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
840385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
840386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
843643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
843643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
844738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
844741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 879.61ns 
844742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
844742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
844743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
848037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
848037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
849136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
849268     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
849300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 160.07ms 
849304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
849304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390ns 
849306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
852571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
852571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
853670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
853739     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
853741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.87ms 
853744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
853744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
853746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
857120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
857120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
858193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
858195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
858230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
858291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
858317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
858326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
858342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
858348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
858351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
858355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
858373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
858377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
858384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
858387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
858682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
858684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
858686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
858693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
858695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
858860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
858862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
858865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
858867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
858869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
858874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
859092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
859095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
859095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
859096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
859098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
859099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
859254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
859256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
859257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
859258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
859259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
859260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
859269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
859270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
859271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
859274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
859275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
859276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
859284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
859285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
859286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
859288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
859288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
859290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
859453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
859455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
859456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
859610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
859612     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)'' 
859614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
859616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
859617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
859620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
859622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
859623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
859627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
859629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
859631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
859632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
859633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
859775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
859780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
859782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
859783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
859784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
859785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
859786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
859947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
859948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
859951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
859953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
859954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
859955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
859955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
859957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
860080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
860082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
860229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
860234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
860241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
860242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
860245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
860246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
860247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
860247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
860248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
860250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
860259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
860266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
860412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
860414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
860415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
860417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
860417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
860418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
860419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
860420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
860487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
860494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
860618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
860620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
860622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
860624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
860625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
860625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
860798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
860803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
860804     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)'' 
860807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
860808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
860809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
860810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
860810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
860823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
860825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
860826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
860827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
860963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
860965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
860965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
860966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
860967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
860968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
861105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
861107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
861108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
861111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
861112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
861113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
861113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
861114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
861225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
861227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
861338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
861340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
861341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
861347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
861352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
861362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
861528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
861529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
861530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
861531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
861545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
861661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
866165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
866166     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)'' 
866172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
866172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
866173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
866174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
866174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
866185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
866186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
866187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
866188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
866188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
866323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
866328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
866330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
866331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
866332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
866334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
866336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
866479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
866480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
866481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
866483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
866483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
866484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
866485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
866486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
866585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
866587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
866680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
866685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
866690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
866691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
866692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
866693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
866705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
866858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
866859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
866860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
866861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
866955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
866967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
866968     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)'' 
866970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
866971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
866971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
866972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
866972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
866986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
866987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
866988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
866989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
866989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
867101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
867102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
867103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
867104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
867105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
867231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
867236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
867237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
867238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
867238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
867239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
867239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
867365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
867366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
867367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
867369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
867369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
867370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
867370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
867371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
867372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
867373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
867374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
867375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
867375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
867375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
867376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
867492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
867494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
867501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
867616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
867726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
867728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
867729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
867729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
867730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
867731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
867731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
867732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
867733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
867850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
867859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
867984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
867985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
867986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
867987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
867988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
867988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
867989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
867990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
867997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
867998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
868105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
868112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
868120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
868256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
868258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
868259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
868260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
868260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
868260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
868261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
868262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
868343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
868344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
868345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
868346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
868346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
868354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
868360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
868526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
868640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
868642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
868642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
868644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
868871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
869051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
869052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
873041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
873046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
873047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
873048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
873049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
873202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
873204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
873205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
873205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
873206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
873351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
877502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
881729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
881734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
881734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
881735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
881736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
881889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
881890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
881891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
881892     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)' ...' 
881894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
883409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
883409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
883410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
886715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
886715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
887836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
887837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
887838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
887848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
887861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
887864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
887866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
887866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
887872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
887873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
887878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
887881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
887882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
887894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
887896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
887897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
887957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
887959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
887959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
887960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
887961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
888045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
888046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
888047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
888048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
888049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
888053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
888054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
888054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
888056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
888057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
888057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
888152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
888154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
888154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
888155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
888156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
888157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
888250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
888251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
888252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
888253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
888253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
888255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
888255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
888256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
888258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
888259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
888260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
888261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
888261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
888262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
888263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
888264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
888264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
888265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
888267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
888270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
888305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
888307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
888361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
888362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
888364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
888365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
888366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
888367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
888419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
888422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
888423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
888425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
888426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
888427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
888427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
888479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
888483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
888487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
888556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
888624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
888624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.5ns 
888625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
891929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
891929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
893058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
893131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.21ms