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

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

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

616        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
635        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.7ms 
833        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
845        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)

1674       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1676       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1680       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1680       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3112       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8271       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.44s 
8336       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8367       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.2ns 
8378       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8379       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.8ns 
8383       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11164      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
11166      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12120      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.17ms 
12150      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12150      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.7ns 
12153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14817      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
14818      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15707      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.52ms 
15710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15710      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.9ns 
15711      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18208      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
18208      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19053      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19059      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
19061      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19061      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.3ns 
19062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21521      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
21521      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22331      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
22334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22334      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.1ns 
22335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24731      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
24731      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25597      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.39ms 
25600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.2ns 
25602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28013      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
28014      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28847      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.72ms 
28849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
28850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31236      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
31236      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32021      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32025      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 711.3ns 
32026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32026      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.2ns 
32027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
34403      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35201      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 599.8ns 
35205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35205      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.9ns 
35206      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37587      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
37587      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38360      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38362      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 564.2ns 
38365      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38365      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.5ns 
38367      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40727      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
40728      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41483      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.3ns 
41488      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41488      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.5ns 
41490      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43870      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
43870      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44635      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44637      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.1ns 
44640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44640      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261ns 
44641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46997      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
46998      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47821      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.07ms 
47823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47823      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.4ns 
47826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50194      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
50195      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50945      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50975      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.1ms 
50977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.8ns 
50978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53366      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
53366      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54134      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54330      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 185.57ms 
54334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54334      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.4ns 
54335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56700      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
56700      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57471      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
57472      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57472      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
57473      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59819      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
59819      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60597      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
60598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60599      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
60599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62937      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
62938      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63761      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.1ms 
63763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63764      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.5ns 
63765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66112      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
66112      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66895      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.25ms 
66897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66897      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.2ns 
66898      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69247      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
69247      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
70017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
70028      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.23ms 
70030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
70030      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.1ns 
70031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72362      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
72362      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
73125      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73142      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.23ms 
73146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73146      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319ns 
73147      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
75485      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76250      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76262      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
76264      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76264      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.9ns 
76265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78596      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
78597      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79387      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.75ms 
79389      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79389      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
79390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81734      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
81734      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82505      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
82506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82507      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns 
82507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84864      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
84864      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85616      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85647      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.26ms 
85649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.6ns 
85651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
88022      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88817      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.09ms 
88819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88820      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.1ns 
88821      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91206      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
91206      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91983      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.6ms 
91985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91985      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.8ns 
91986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94363      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
94363      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
95110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
95117      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.44ms 
95119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
95119      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
95120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97481      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
97481      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
98253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
98269      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.39ms 
98271      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
98272      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.5ns 
98273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
100608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
101370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
101380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ms 
101382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
101383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.4ns 
101384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
103707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
104474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
104482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 514.4ns 
104484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
106831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
107609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
107617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
107619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
107620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 586.5ns 
107621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
109960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
110723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
110728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
110730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
110730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
110730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
113069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
113854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
113855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
116189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.08ms 
116957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
116958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
119285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
120042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
120072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.79ms 
120073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
120073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
120074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
122445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
123204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
123218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.19ms 
123221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
123221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.6ns 
123222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
125537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
126305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
126318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.67ms 
126319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
126320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.4ns 
126320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
128664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
129427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
129440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.82ms 
129441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
129441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
129442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
131785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
132522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
132534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.41ms 
132535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
132536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
132536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
134883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
135624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
135651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.33ms 
135652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
135652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.8ns 
135653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
138012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
138771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
138774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.7ns 
138775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
138775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
138776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
141129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
141877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
141881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
141882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
141882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
141883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
144231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
144990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
144996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
144998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
144998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
144998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
147315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
148077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
148083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
148084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
148084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
148085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
150405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
151167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
151181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.89ms 
151182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
151182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
151183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
153496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
154253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
154259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
154260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
154260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
154261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
156610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
157369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
157372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 874.8ns 
157374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
157375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.1ns 
157376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
159704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
160465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
160468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
160470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
160470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.3ns 
160470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
162779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
163534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
163537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
163538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
163538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
163539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
165854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
166613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
166662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.02ms 
166668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
166668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.8ns 
166670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
168977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
169733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
169791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.31ms 
169792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
169793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
169793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
172110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
172867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
172870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
172871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
172871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
172872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
175198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
175934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
175959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.1ms 
175960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
175960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184ns 
175961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
178287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
179024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
179042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.03ms 
179044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
179044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
179045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
181400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
182141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
182144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.9ns 
182145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
182145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
182146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
184477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
185214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
185343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 118.33ms 
185346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
185346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.6ns 
185347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
187682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
188443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
188450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
188452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
188452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
188452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
190776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
191534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
191539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
191540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
191540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
191541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
193853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
194609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
194622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
194623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
194623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns 
194624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
196945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
197703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
197713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
197715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
197716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.2ns 
197716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
200032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
200785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
200789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
200790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
200790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
200790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
203102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
203859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
203862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
203863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
203863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
203864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
206181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
206937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
206950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.67ms 
206951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
206952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
206952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
209266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
210028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
210038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.59ms 
210040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
210040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
210040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
212348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
213102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
213112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.58ms 
213114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
213114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
213115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
215419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
216176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
216178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 808.8ns 
216179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
216180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
216180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
218517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
219253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
219256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
219257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
219257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
219258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
221587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
222322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
222326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
222327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
222327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
222328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
224651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
225388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
225390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 727.9ns 
225391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
225391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
225392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
227728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
228464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
228466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 396.4ns 
228467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
228467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
228468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
230795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
231557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
231560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
231561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
231561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
231562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
233879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
234634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
234636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.6ns 
234637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
234638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
234638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
236951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
237709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
237765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.38ms 
237766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
237766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
237767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
240095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
240855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
240880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.93ms 
240881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
240881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
240882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
243216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
243977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
243996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.58ms 
243997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
243997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
243998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
246317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
247071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
247097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.81ms 
247098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
247098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
247099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
249409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
250165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
250181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.66ms 
250182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
250183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
250183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
252492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
253248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
253278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.63ms 
253279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
253279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
253280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
255595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
256353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
256369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.57ms 
256370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
256370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
256371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
258679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
259441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
259453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ms 
259454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
259454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
259455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
261790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
262535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
262558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.12ms 
262565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
262566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.6ns 
262567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
264906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
265641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
265653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 
265654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
265654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
265655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
267986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
268725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
268741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
268742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
268742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
268743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
271072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
271809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
271824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.66ms 
271825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
271825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
271826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
274148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
274905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
274920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.71ms 
274921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
274922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
274922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
277234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
277990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
278004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.29ms 
278005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
278005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
278006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
280312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
281069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
281082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
281083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
281083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
281084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
283397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
284150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
284165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.75ms 
284166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
284166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
284167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
286479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
287235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
287249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ms 
287251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
287251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
287251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
289562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
290321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
290330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
290333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
290333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
290334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
292657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
293414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
293424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.03ms 
293426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
293426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
293426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
295746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
296502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
296505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
296506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
296507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
296507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
298820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
299577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
299579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.8ns 
299581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
299581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.7ns 
299582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
301885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
302644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
302646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618ns 
302647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
302647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
302648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
304976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
305713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
305719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
305720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
305721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.4ns 
305721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
308059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
308794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
308799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
308801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
308801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.7ns 
308802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
311140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
311876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
311885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.01ms 
311886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
311887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
311887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
314223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
314958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
314962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
314963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
314963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.4ns 
314964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
317294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
318029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
318031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 402.6ns 
318032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
318032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
318033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
320364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
321120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
321124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
321125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
321126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
321126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
323445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
324200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
324202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 441.4ns 
324203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
324204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
324204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
326514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
327275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
327277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 417.4ns 
327278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
327278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
327278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
329594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
330348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
330350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 449.4ns 
330351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
330351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
330352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
332664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
333419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
333422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
333423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
333423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
333424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
335734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
336491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
336505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
336507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
336507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.5ns 
336508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
338834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
339590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
339593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
339594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
339594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
339594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
341900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
342657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
342662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
342663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
342663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
342664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
344971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
345727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
345730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
345731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
345732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
345732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
348035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
348791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
348802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.43ms 
348803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
348803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
348804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
351132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
351868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
351871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
351872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
351872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
351872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
354195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
354932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
354934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 839.3ns 
354935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
354935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
354936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
357259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
357994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
357998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
357999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
357999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
357999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
360325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
361060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
361073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.96ms 
361074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
361074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
361075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
363397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
364130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
364134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 339.6ns 
364135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
364135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
364136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
366454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
367205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
367229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.76ms 
367230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
367230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
367231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
369537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
370294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
370297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
370298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
370298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
370298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
372605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
373362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
373375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.97ms 
373377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
373377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
373377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
375684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
376440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
376454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.59ms 
376455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
376455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
376456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
378771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
379528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
379544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.38ms 
379545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
379545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
379546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
381861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
382619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
382621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 419.9ns 
382622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
382622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
382623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
384935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
385691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
385696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
385697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
385697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
385698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
388001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
388761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
388764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
388765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
388765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
388765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
391075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
391833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
391835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.5ns 
391836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
391836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.2ns 
391837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
394135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
394892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
394894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.9ns 
394895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
394895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
394896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
397227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
397968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
397970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 968.1ns 
397971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
397971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
397972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
400298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
401038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
401041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 958.6ns 
401042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
401042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
401043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
403368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
404130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
404138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
404139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
404139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
404140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
406450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
407211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
407217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms 
407219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
407219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
407219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
409525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
410291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
410297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
410300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
410300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
410301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
412619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
413381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
413388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
413389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
413389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
413390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
415693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
416456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
416459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
416460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
416461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
416461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
418824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
419570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
419575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
419576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
419576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.8ns 
419577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
421908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
422652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
422654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.7ns 
422656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
422656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
422656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
424980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
425747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
425749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 868.3ns 
425751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
425751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
425751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
428055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
428817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
428820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 862.9ns 
428821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
428821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.1ns 
428821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
431119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
431881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
431889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
431890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
431890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
431891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
434187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
434950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
434952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 975.89ns 
434953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
434953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
434954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
437272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
438014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
438019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
438021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
438021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.7ns 
438022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
440353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
441116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
441118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 677ns 
441120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
441120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
441121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
443429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
444191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
444193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 593.1ns 
444194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
444194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
444195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
446496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
447260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
447262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
447264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
447264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
447264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
449587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
450331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
450333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667ns 
450334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
450334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
450335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
452656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
453425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
453427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 914.6ns 
453428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
453429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
453429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
455734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
456499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
456501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822ns 
456502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
456502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
456503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
458807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
459572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
459575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
459576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
459576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
459577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
461904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
462649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
462651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 705.4ns 
462652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
462652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
462653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
464970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
465733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
465741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.83ms 
465742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
465742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
465742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
468050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
468815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
468817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 453.8ns 
468818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
468818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
468819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
471157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
471902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
471907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
471909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
471909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
471910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
474234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
475002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
475004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
475005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
475005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
475006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
477315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
478081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
478083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 576.7ns 
478084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
478084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
478085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
480408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
481152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
481155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
481156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
481156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
481157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
483479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
484243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
484245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 841.3ns 
484246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
484246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
484247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
486555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
487320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
487323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
487324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
487324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
487325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
489645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
490390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
490392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 955ns 
490393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
490393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
490394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
492711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
493476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
493479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
493480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
493480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
493481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
495787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
496550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
496557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.87ms 
496558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
496558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 559.3ns 
496559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
498883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
499646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
499653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
499654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
499654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
499655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
501964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
502727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
502732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
502734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
502734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
502734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
505054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
505815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
505821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
505822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
505822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
505823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
508120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
508885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
508897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms 
508899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
508899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.8ns 
508900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
511215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
511957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
511967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
511968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
511968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
511969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
514285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
515049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
515058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.66ms 
515059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
515059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
515060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
517382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
518125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
518132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
518133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
518133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
518133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
520449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
521211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
521230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.3ms 
521231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
521231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
521232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
523545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
524288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
524308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.79ms 
524309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
524310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
524310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
526623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
527384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
527402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.85ms 
527403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
527403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
527404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
529718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
530461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
530478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.89ms 
530479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
530479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
530480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
532793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
533555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
533573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.46ms 
533574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
533574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
533575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
535890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
536635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
536708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.78ms 
536709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
536709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
536710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
539012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
539777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
539781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
539783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
539783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
539783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
542098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
542860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
542865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
542866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
542866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
542867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
545169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
545935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
545938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
545939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
545939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
545940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
548258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
549020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
549032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.88ms 
549033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
549033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
549034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
551353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
552097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
552103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
552104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
552104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
552105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
554422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
555185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
555188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
555189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
555189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
555190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
557499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
558260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
558269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.97ms 
558271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
558271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
558271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
560576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
561339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
561349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.48ms 
561350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
561350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
561351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
563677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
564444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
564457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
564458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
564458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
564459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
566784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
567548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
567550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 866.7ns 
567551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
567551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
567552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
569856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
570622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
570625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
570626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
570626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
570627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
572949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
573714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
573719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
573720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
573720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
573720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
576046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
576810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
576814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
576815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
576815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
576816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
579127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
579892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
579932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.39ms 
579933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
579933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
579934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
582278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
583044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
583063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.21ms 
583065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
583066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.8ns 
583066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
585393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
586157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
586167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.03ms 
586169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
586169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
586169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
588490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
589241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
589243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 207.2ns 
589245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
589245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.6ns 
589246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
591575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
592343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
592417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.43ms 
592419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
592419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
592420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
594744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
595512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
595543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.38ms 
595544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
595544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
595545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
597867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
598634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
598636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 231.8ns 
598637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
598637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
598637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
600965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
601731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
601733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.5ns 
601734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
601734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
601735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
604044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
604810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
604812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.3ns 
604813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
604813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
604813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
607135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
607900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
607902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 322.7ns 
607903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
607903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
607904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
610223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
610985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
611070     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
611077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.6ms 
611079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
611079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
611080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
613402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
614164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
614204     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
614205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.76ms 
614206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
614206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
614207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
616536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
617301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
617302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ns 
617327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
617394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
617410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
617417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
617431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
617432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
617434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
617435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
617442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
617443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
617448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
617450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
617681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
617682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
617683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
617684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
617685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
617790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
617791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
617792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
617793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
617794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
617795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
617957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
617958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
617960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
617960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
617961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
617962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
618099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
618100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
618101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
618102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
618103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
618104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
618110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
618111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
618112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
618113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
618114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
618115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
618122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
618122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
618123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
618124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
618124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
618125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
618248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
618249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
618250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
618369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
618370     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)'' 
618371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
618373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
618374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
618374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
618375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
618376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
618380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
618380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
618382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
618383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
618384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
618483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
618486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
618487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
618488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
618489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
618489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
618490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
618595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
618596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
618597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
618598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
618599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
618599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
618600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
618601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
618690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
618692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
618773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
618778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
618782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
618782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
618783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
618784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
618785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
618786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
618786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
618787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
618794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
618798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
618889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
618890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
618891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
618892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
618893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
618894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
618894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
618895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
618945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
618951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
619044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
619045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
619046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
619048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
619049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
619050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
619171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
619175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
619176     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)'' 
619177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
619179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
619180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
619180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
619181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
619190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
619190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
619192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
619193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
619281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
619282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
619283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
619284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
619284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
619285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
619385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
619386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
619387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
619388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
619389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
619389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
619390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
619391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
619470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
619471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
619547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
619548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
619549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
619553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
619556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
619560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
619727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
619728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
619729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
619731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
619740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
619830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
622990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
622990     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)'' 
622994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
622996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
622996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
622997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
622997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
623004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
623005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
623006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
623007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
623007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
623094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
623097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
623098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
623098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
623099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
623099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
623100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
623188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
623189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
623190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
623191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
623192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
623192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
623193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
623193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
623263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
623264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
623333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
623336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
623340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
623341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
623342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
623342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
623352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
623427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
623428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
623429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
623429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
623497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
623506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
623506     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)'' 
623507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
623508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
623509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
623509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
623509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
623519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
623520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
623521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
623522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
623522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
623644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
623644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
623645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
623646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
623647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
623730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
623734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
623735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
623735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
623736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
623736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
623737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
623827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
623828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
623829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
623829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
623830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
623830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
623831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
623831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
623832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
623832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
623833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
623834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
623834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
623834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
623835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
623915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
623916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
623921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
623992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
624065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
624066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
624067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
624067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
624068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
624068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
624069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
624069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
624069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
624148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
624153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
624235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
624236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
624237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
624237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
624238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
624238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
624238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
624239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
624243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
624244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
624317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
624321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
624326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
624418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
624418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
624419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
624420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
624420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
624421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
624421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
624421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
624472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
624472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
624473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
624473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
624474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
624479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
624484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
624591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
624673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
624674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
624674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
624675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
624832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
624914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
624914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
627703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
627707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
627708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
627709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
627710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
627815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
627816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
627817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
627818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
627819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
627916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
630673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
633568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
633572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
633573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
633574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
633575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
633681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
633682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
633683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
633684     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)' ...' 
633685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
634750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
634750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
634751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
637128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
637915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
637916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
637916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
637925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
637933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
637935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
637937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
637939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
637944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
637944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
637948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
637949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
637951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
637961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
637961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
637963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
638009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
638009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
638010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
638010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
638011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
638077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
638078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
638078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
638079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
638080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
638083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
638083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
638084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
638084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
638085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
638086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
638171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
638171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
638172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
638172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
638173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
638174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
638259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
638259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
638260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
638260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
638261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
638261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
638262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
638262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
638263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
638263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
638263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
638264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
638264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
638264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
638265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
638265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
638265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
638266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
638266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
638269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
638306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
638307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
638368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
638369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
638370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
638371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
638372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
638372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
638430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
638432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
638433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
638434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
638435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
638436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
638436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
638490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
638492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
638495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
638543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
638591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
638591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
638591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
640961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
641742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
641757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.13ms