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

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

Test	Method name	Duration	Result
powPositive	data()[100]	2.935s	passed
powPositiveConcrete	data()[101]	2.981s	passed
powGeq1Concrete	data()[102]	2.962s	passed
pow2InIntLower	data()[103]	2.959s	passed
pow2InIntUpper	data()[104]	3.001s	passed
logSelfConcrete	data()[105]	2.993s	passed
log1Concrete	data()[106]	2.973s	passed
logProduct	data()[107]	2.987s	passed
logTimesBaseConcrete	data()[108]	2.982s	passed
logProdIdentity	data()[109]	2.959s	passed
moduloByteIsInByte	data()[10]	3.013s	passed
logProdIdentityConcrete	data()[110]	2.948s	passed
logPowIdentity	data()[111]	2.967s	passed
logPowIdentityConcrete	data()[112]	2.946s	passed
logPositive	data()[113]	2.957s	passed
logPositiveConcrete	data()[114]	2.959s	passed
logMono	data()[115]	2.951s	passed
logMonoConcrete	data()[116]	2.934s	passed
powLogLess	data()[117]	3.028s	passed
powLogMore2	data()[118]	2.951s	passed
logLessThanPow	data()[119]	2.976s	passed
moduloCharIsInChar	data()[11]	3.030s	passed
logLessThanPowConcrete	data()[120]	2.952s	passed
logSqueeze	data()[121]	2.950s	passed
ifthenelse_equals	data()[122]	2.969s	passed
ifthenelse_equals_1	data()[123]	2.941s	passed
ifthenelse_equals_2	data()[124]	2.952s	passed
disjointWithSingleton1	data()[125]	2.941s	passed
disjointWithSingleton2	data()[126]	2.956s	passed
disjointArrayRanges	data()[127]	2.955s	passed
disjointArrayRangeAllFields1	data()[128]	2.957s	passed
disjointArrayRangeAllFields2	data()[129]	2.950s	passed
div_unique1	data()[12]	3.110s	passed
seqSelfDefinition	data()[130]	2.981s	passed
seqOutsideValue	data()[131]	2.952s	passed
castedGetAny	data()[132]	2.960s	passed
seqGetAlphaCast	data()[133]	2.941s	passed
getOfSeqSingleton	data()[134]	2.964s	passed
getOfSeqSingletonConcrete	data()[135]	2.955s	passed
getOfSeqConcat	data()[136]	2.961s	passed
getOfSeqSub	data()[137]	2.961s	passed
getOfSeqReverse	data()[138]	2.950s	passed
lenOfSeqEmpty	data()[139]	2.967s	passed
div_unique2	data()[13]	3.014s	passed
lenOfSeqSingleton	data()[140]	2.938s	passed
lenOfSeqConcat	data()[141]	2.965s	passed
lenOfSeqSub	data()[142]	2.956s	passed
lenOfSeqReverse	data()[143]	2.942s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	2.956s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	2.961s	passed
getOfSeqSingletonEQ	data()[146]	2.954s	passed
getOfSeqConcatEQ	data()[147]	2.976s	passed
getOfSeqSubEQ	data()[148]	2.975s	passed
getOfSeqReverseEQ	data()[149]	2.975s	passed
div_exists	data()[14]	3.170s	passed
lenOfSeqEmptyEQ	data()[150]	2.957s	passed
lenOfSeqSingletonEQ	data()[151]	2.962s	passed
lenOfSeqConcatEQ	data()[152]	2.973s	passed
lenOfSeqSubEQ	data()[153]	2.961s	passed
lenOfSeqReverseEQ	data()[154]	2.935s	passed
getOfSeqDefEQ	data()[155]	2.949s	passed
lenOfSeqDefEQ	data()[156]	2.963s	passed
seqConcatWithSeqEmpty1	data()[157]	2.963s	passed
seqConcatWithSeqEmpty2	data()[158]	2.964s	passed
seqReverseOfSeqEmpty	data()[159]	2.975s	passed
div_one	data()[15]	2.987s	passed
subSeqComplete	data()[160]	2.950s	passed
subSeqTailR	data()[161]	2.971s	passed
subSeqTailL	data()[162]	2.974s	passed
subSeqTailEQR	data()[163]	2.989s	passed
subSeqTailEQL	data()[164]	2.970s	passed
seqDef_split	data()[165]	3.007s	passed
seqDef_induction_upper	data()[166]	2.999s	passed
seqDef_induction_upper_concrete	data()[167]	2.999s	passed
seqDef_induction_lower	data()[168]	3.011s	passed
seqDef_induction_lower_concrete	data()[169]	2.983s	passed
jdiv_one	data()[16]	3.001s	passed
seqDef_split_in_three	data()[170]	3.007s	passed
seqDef_empty	data()[171]	2.970s	passed
seqDef_one_summand	data()[172]	2.958s	passed
seqDef_lower_equals_upper	data()[173]	2.962s	passed
seqDefOfSeq	data()[174]	2.975s	passed
seqSelfDefinitionEQ2	data()[175]	2.972s	passed
indexOfSeqSingleton	data()[176]	2.958s	passed
indexOfSeqConcatFirst	data()[177]	2.975s	passed
indexOfSeqConcatSecond	data()[178]	2.962s	passed
indexOfSeqSub	data()[179]	2.968s	passed
div_zero	data()[17]	3.033s	passed
lenOfArray2seq	data()[180]	2.956s	passed
getAnyOfArray2seq	data()[181]	2.959s	passed
getOfArray2seq	data()[182]	2.960s	passed
getAnyOfNPermInv	data()[183]	2.972s	passed
seqNPermRange	data()[184]	2.996s	passed
seqPermTrans	data()[185]	2.980s	passed
seqPermRefl	data()[186]	2.968s	passed
seqPermSplit	data()[187]	2.987s	passed
seqNPermRight	data()[188]	3.040s	passed
seqPermFromSwap	data()[189]	2.999s	passed
divResZero1	data()[18]	3.025s	passed
seqPermTransAlt0	data()[190]	2.979s	passed
seqPermTransAlt1	data()[191]	2.960s	passed
seqPermTransAlt2	data()[192]	2.958s	passed
seqPermTransAlt3	data()[193]	2.974s	passed
seqPermForall	data()[194]	3.053s	passed
seqPermExists	data()[195]	3.004s	passed
schiffl_lemma_2	data()[196]	21.018s	passed
schiffl_thm_1	data()[197]	3.892s	passed
eqSameSeq	data()[198]	2.984s	passed
divResZero2	data()[19]	2.985s	passed
eqTermCut	data()[1]	3.552s	passed
divResOne1	data()[20]	2.988s	passed
divResOne2	data()[21]	2.989s	passed
div_cancel1	data()[22]	2.997s	passed
div_cancel2	data()[23]	3.000s	passed
divAddMultDenom	data()[24]	3.011s	passed
divMinus	data()[25]	3.010s	passed
divMinusDenom	data()[26]	2.996s	passed
divLeastDPos	data()[27]	2.972s	passed
divLeastDNeg	data()[28]	2.975s	passed
divGreatestDPos	data()[29]	2.961s	passed
equivAllRight	data()[2]	3.313s	passed
divGreatestDNeg	data()[30]	2.953s	passed
divIncreasingPos	data()[31]	2.970s	passed
divIncreasingNeg	data()[32]	2.965s	passed
jdiv_zero	data()[33]	2.958s	passed
jdivPulloutMinusNum	data()[34]	2.987s	passed
jdivPulloutMinusDenom	data()[35]	2.996s	passed
jdiv_uniquePosPos	data()[36]	2.954s	passed
jdiv_uniquePosNeg	data()[37]	2.957s	passed
jdiv_uniqueNegPos	data()[38]	2.984s	passed
jdiv_uniqueNegNeg	data()[39]	2.953s	passed
irrflConcrete1	data()[3]	3.267s	passed
jdivMultDenom1	data()[40]	2.995s	passed
jdivMultDenom2	data()[41]	2.974s	passed
mod_geZero	data()[42]	2.951s	passed
mod_lessDenom	data()[43]	2.975s	passed
jmod_NumPos	data()[44]	2.968s	passed
jmod_NumNeg	data()[45]	2.962s	passed
jmod_geZero	data()[46]	2.952s	passed
jmodNumZero	data()[47]	2.937s	passed
jmod_pulloutminusNum	data()[48]	2.983s	passed
jmod_pulloutminusDenom	data()[49]	2.949s	passed
irrflConcrete2	data()[4]	3.243s	passed
jmodUnique1	data()[50]	3.017s	passed
jmodUnique2	data()[51]	3.050s	passed
intDivRem	data()[52]	2.951s	passed
jmodjmod	data()[53]	2.965s	passed
jmodDivisible	data()[54]	2.970s	passed
jmodDivisibleRep	data()[55]	2.940s	passed
jdivAddMultDenom	data()[56]	3.027s	passed
jmodAltZero	data()[57]	2.996s	passed
jmodAddMultDenomZero	data()[58]	2.971s	passed
polyDiv_zero	data()[59]	2.962s	passed
cancel_gtPos	data()[5]	3.143s	passed
polyMod_ltdivDenom	data()[60]	2.945s	passed
bsum_empty	data()[61]	2.942s	passed
bsum_induction_upper	data()[62]	2.932s	passed
bsum_induction_lower	data()[63]	2.951s	passed
bsum_num_of_bounds	data()[64]	2.975s	passed
bsum_num_of_bounds2	data()[65]	2.951s	passed
bsum_induction_upper2	data()[66]	2.941s	passed
bsum_induction_upper_concrete	data()[67]	2.939s	passed
bsum_induction_upper_concrete_2	data()[68]	2.950s	passed
bsum_induction_upper2_concrete	data()[69]	2.928s	passed
cancel_gtNeg	data()[6]	3.082s	passed
bsum_induction_lower_concrete	data()[70]	2.933s	passed
bsum_induction_lower2	data()[71]	2.952s	passed
bsum_induction_lower2_concrete	data()[72]	2.931s	passed
bsum_positive	data()[73]	2.960s	passed
bsum_upper_bound	data()[74]	2.990s	passed
bsum_lower_bound	data()[75]	2.959s	passed
bsum_positive_lower_bound_element	data()[76]	2.959s	passed
bsum_sub_same_index	data()[77]	2.953s	passed
bsum_less_same_index	data()[78]	2.987s	passed
bsum_equal_except_one_index	data()[79]	2.945s	passed
moduloIntIsInInt	data()[7]	3.081s	passed
bsum_num_of_is_max	data()[80]	2.947s	passed
bsum_num_of_is_max2	data()[81]	2.978s	passed
bsum_num_of_is_max3	data()[82]	2.945s	passed
bsum_num_of_is_max4	data()[83]	2.944s	passed
bsum_num_of_lt_max	data()[84]	2.968s	passed
bsum_num_of_lt_max2	data()[85]	2.956s	passed
bsum_num_of_lt_max3	data()[86]	2.943s	passed
bsum_num_of_lt_max4	data()[87]	2.993s	passed
bsum_num_of_gt0	data()[88]	2.941s	passed
bsum_num_of_gt0_alt	data()[89]	2.952s	passed
moduloLongIsInLong	data()[8]	3.056s	passed
bsum_add_concrete	data()[90]	2.948s	passed
bprod_all_positive	data()[91]	2.968s	passed
bprod_split	data()[92]	2.938s	passed
powConcrete0	data()[93]	2.926s	passed
powConcrete1	data()[94]	2.961s	passed
powSplitFactor	data()[95]	2.943s	passed
powAdd	data()[96]	2.949s	passed
powMono	data()[97]	2.949s	passed
powMonoConcrete	data()[98]	2.964s	passed
powMonoConcreteRight	data()[99]	2.937s	passed
moduloShortIsInShort	data()[9]	3.030s	passed
Standard output

723        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
748        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.55ms 
977        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
996        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)

1844       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1847       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1849       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1849       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3274       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8194       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.22s 
8262       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8293       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.4ns 
8308       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8308       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.6ns 
8313       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10935      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
10937      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11849      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.68ms 
11857      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11858      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.5ns 
11859      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14323      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
14323      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15168      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
15171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15172      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.5ns 
15173      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
17567      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18435      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.09ms 
18440      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18441      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 596.29ns 
18442      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20864      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
20865      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21676      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21681      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
21683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21683      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.3ns 
21685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23989      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
23990      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24786      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24823      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.76ms 
24827      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24827      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.4ns 
24828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27112      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
27113      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27890      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27907      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.61ms 
27911      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27912      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.3ns 
27913      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30205      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
30207      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
30985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
30988      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 890.99ns 
30991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
30991      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.6ns 
30992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33285      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
33286      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34045      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 565.79ns 
34047      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34047      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.9ns 
34048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36307      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
36307      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37072      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37075      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 583.59ns 
37077      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37077      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.1ns 
37078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39357      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
39358      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40088      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 614.7ns 
40090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40091      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.9ns 
40092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42370      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
42371      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
43116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
43118      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.6ns 
43120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
43121      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332ns 
43122      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45439      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
45440      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
46182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
46228      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.83ms 
46231      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
46232      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382ns 
46233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48478      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
48478      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
49214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
49242      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.52ms 
49244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
49245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.2ns 
49246      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51500      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
51500      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
52243      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
52402      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 150.34ms 
52413      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
52414      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.9ns 
52415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54653      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
54654      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
55391      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
55399      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
55402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
55402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns 
55403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57639      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
57640      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
58397      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
58400      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
58404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
58405      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 484.1ns 
58406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60668      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
60669      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
61385      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
61434      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.55ms 
61438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
61438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.1ns 
61440      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63714      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
63715      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
64449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
64461      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.87ms 
64463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
64463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
64463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66698      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
66698      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
67436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
67446      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.16ms 
67448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
67448      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.6ns 
67449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69709      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
69709      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
70423      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
70435      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.01ms 
70436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
70436      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
70437      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72678      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
72678      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
73412      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
73424      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
73425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
73425      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
73426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75662      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
75662      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
76403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
76420      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.05ms 
76421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
76421      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
76422      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
78673      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
79417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
79420      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
79422      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
79423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.7ns 
79424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
81665      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
82401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
82431      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.08ms 
82433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
82433      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.7ns 
82435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84662      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
84662      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
85397      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
85441      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.71ms 
85444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
85444      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313ns 
85445      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
87676      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
88409      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
88438      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.7ms 
88439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
88439      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
88440      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90692      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
90692      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
91403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
91410      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms 
91411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
91411      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
91412      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93645      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
93645      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
94374      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
94385      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.42ms 
94386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
94386      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
94387      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96606      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
96606      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
97336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
97346      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.05ms 
97347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
97347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.9ns 
97348      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99583      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
99583      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
100293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
100299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
100301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
100301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
100301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
102535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
103263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
103270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
103271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
103271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
103272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
105498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
106229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
106235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
106236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
106236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
106237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
108459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
109189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
109192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
109193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
109193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
109194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
111438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
112169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
112179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.27ms 
112181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
112181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300ns 
112182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
114413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
115145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
115175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.59ms 
115176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
115176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
115177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
117387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
118116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
118129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.44ms 
118131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
118131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
118132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
120361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
121073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
121086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.05ms 
121087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
121088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
121088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
123330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
124057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
124071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ms 
124072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
124072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
124073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
126278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
127010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
127023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.93ms 
127024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
127025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
127025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
129263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
129973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
130017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.39ms 
130021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
130022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 590.5ns 
130024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
132264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
132991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
132993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.59ns 
132994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
132994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
132995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
135207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
135941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
135945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
135947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
135947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.9ns 
135948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
138172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
138908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
138920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.44ms 
138922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
138922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.1ns 
138924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
141154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
141882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
141888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.52ms 
141890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
141890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.9ns 
141891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
144098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
144828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
144850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.01ms 
144853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
144853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.5ns 
144854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
147071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
147797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
147803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
147804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
147805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
147805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
150031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
150737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
150740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
150742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
150743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.2ns 
150743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
152989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
153721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
153724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
153725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
153725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
153726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
155942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
156669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
156672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
156673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
156674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
156674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
158912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
159618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
159688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.54ms 
159694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
159694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.1ns 
159695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
161931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
162659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
162742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.93ms 
162745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
162746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.9ns 
162747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
164968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
165692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
165695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
165696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
165696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.4ns 
165697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
167901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
168633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
168659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.86ms 
168661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
168661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.5ns 
168662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
170886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
171611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
171630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.82ms 
171631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
171631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.6ns 
171632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
173842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
174567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
174570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
174571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
174571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
174572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
176774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
177501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
177596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.15ms 
177598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
177598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.7ns 
177599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
179849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
180584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
180593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.15ms 
180595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
180595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.2ns 
180596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
182825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
183559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
183564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
183565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
183566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
183566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
185777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
186504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
186526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.32ms 
186528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
186529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.1ns 
186529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
188756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
189462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
189471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.42ms 
189473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
189473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
189474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
191690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
192411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
192414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
192415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
192415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
192416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
194617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
195342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
195346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
195347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
195347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
195348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
197558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
198284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
198297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.55ms 
198299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
198299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
198300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
200536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
201263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
201274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
201275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
201275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
201276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
203488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
204215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
204225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.08ms 
204227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
204227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
204227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
206434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
207163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
207166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 806.19ns 
207167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
207168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
207168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
209399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
210103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
210106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
210107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
210107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
210108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
212326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
213051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
213055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
213056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
213056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
213057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
215258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
215982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
215984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.49ns 
215985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
215985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
215986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
218210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
218915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
218917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 407.8ns 
218918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
218918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
218919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
221141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
221867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
221870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
221871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
221871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
221871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
224076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
224798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
224801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 726.79ns 
224802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
224802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
224802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
227001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
227727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
227760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.93ms 
227762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
227762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
227762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
229995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
230720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
230750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.7ms 
230752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
230752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.1ns 
230753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
232961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
233684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
233709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.89ms 
233712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
233712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
233713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
235914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
236638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
236669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.83ms 
236670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
236670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
236671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
238896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
239601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
239622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.81ms 
239624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
239624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
239624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
241848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
242572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
242608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.21ms 
242609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
242610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
242610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
244808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
245537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
245554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.2ms 
245555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
245555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
245556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
247783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
248489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
248501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.75ms 
248502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
248502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
248503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
250741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
251465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
251480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.66ms 
251481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
251481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
251482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
253688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
254414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
254426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
254427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
254427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
254427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
256650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
257354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
257370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms 
257371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
257371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
257372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
259597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
260323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
260337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.94ms 
260339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
260339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
260340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
262553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
263278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
263294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.87ms 
263295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
263295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
263296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
265497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
266222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
266236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.42ms 
266237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
266238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
266238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
268475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
269186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
269229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.11ms 
269232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
269232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226ns 
269233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
271435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
272158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
272172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ms 
272173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
272173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
272173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
274374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
275105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
275124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.37ms 
275125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
275126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
275126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
277360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
278066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
278071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 
278073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
278073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
278073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
280303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
281029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
281040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.97ms 
281041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
281041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
281042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
283248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
283975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
283978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
283979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
283979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
283979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
286197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
286902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
286904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 528.2ns 
286905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
286905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
286906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
289131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
289862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
289865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.2ns 
289867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
289867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182ns 
289868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
292077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
292804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
292809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
292810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
292810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
292811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
295022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
295752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
295758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
295760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
295760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.2ns 
295761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
297991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
298699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
298708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
298709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
298709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
298710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
300937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
301668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
301672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
301673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
301673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
301673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
303880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
304607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
304609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 385.8ns 
304610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
304610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
304610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
306831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
307539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
307544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
307545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
307545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
307546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
309791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
310523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
310525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 514.1ns 
310527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
310527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
310527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
312751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
313485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
313487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 526.1ns 
313492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
313492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
313492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
315720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
316448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
316450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 469.6ns 
316451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
316451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
316452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
318707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
319447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
319451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
319453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
319453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.3ns 
319454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
321705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
322438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
322445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
322446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
322446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
322447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
324679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
325413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
325417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
325418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
325418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
325419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
327689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
328400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
328405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
328406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
328406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
328407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
330655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
331384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
331387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
331388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
331388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
331389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
333604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
334334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
334346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms 
334348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
334348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.4ns 
334349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
336584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
337292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
337295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
337296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
337296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
337297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
339532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
340260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
340262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.09ns 
340264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
340264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
340264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
342473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
343203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
343208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
343210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
343210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165ns 
343211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
345442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
346152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
346165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.54ms 
346167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
346167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.3ns 
346168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
348396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
349121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
349125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 279.9ns 
349126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
349127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
349127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
351329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
352053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
352076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.64ms 
352078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
352078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
352078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
354302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
355007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
355010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
355011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
355011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
355012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
357281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
358024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
358038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.19ms 
358040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
358040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179ns 
358041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
360249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
360976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
360989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.37ms 
360990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
360991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
360991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
363222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
363946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
363965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.92ms 
363967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
363967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
363967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
366185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
366915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
366918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 551.29ns 
366919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
366919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
366920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
369155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
369862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
369867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
369870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
369870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.78ns 
369871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
372106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
372835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
372838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
372839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
372839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
372840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
375046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
375777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
375779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 639.19ns 
375780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
375780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
375781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
378004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
378730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
378732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 634.27ns 
378733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
378733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
378734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
380939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
381671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
381674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 946.99ns 
381675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
381675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
381675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
383901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
384628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
384630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 956.39ns 
384631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
384631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
384632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
386846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
387578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
387584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 
387586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
387586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
387587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
389806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
390535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
390541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.96ms 
390543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
390543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
390544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
392750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
393486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
393492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
393493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
393493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
393494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
395733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
396466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
396473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
396475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
396475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.2ns 
396476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
398685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
399421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
399424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
399425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
399425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
399426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
401650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
402381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
402385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
402386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
402386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
402387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
404592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
405324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
405327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.69ns 
405328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
405328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
405328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
407555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
408289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
408291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 750.69ns 
408292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
408292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
408293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
410526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
411244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
411246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 710.49ns 
411247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
411247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
411247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
413468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
414200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
414207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.51ms 
414208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
414208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
414209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
416435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
417165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
417167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
417168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
417169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
417169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
419379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
420113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
420118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
420120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
420120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.6ns 
420121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
422352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
423084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
423086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 780.09ns 
423087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
423087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
423087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
425308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
426023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
426025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 526.7ns 
426026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
426026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
426026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
428253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
428986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
428989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
428991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
428991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.9ns 
428992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
431212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
431944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
431946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 658.59ns 
431947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
431947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.6ns 
431948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
434171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
434886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
434888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 925.29ns 
434889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
434889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
434890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
437110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
437842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
437845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 800.59ns 
437846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
437846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
437846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
440068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
440800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
440805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
440807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
440807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
440808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
443043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
443759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
443761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 749.19ns 
443762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
443762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
443763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
445992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
446729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
446737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
446738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
446738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
446738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
448976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
449710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
449712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 412.19ns 
449713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
449713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
449714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
451949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
452681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
452686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
452688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
452688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
452688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
454908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
455642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
455644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 706.09ns 
455645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
455646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
455646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
457872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
458605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
458607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 567.49ns 
458608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
458608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
458608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
460844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
461577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
461580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
461581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
461582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
461582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
463805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
464538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
464540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.49ns 
464541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
464541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
464542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
466760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
467473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
467476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
467477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
467477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
467478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
469691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
470423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
470426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
470427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
470427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
470428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
472653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
473385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
473389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
473390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
473390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
473391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
475613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
476345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
476352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.78ms 
476353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
476353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
476353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
478576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
479309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
479316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.25ms 
479317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
479317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
479317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
481546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
482285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
482291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
482292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
482292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
482293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
484522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
485236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
485242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 
485243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
485243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
485243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
487469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
488203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
488213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
488214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
488214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
488214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
490442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
491178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
491188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.21ms 
491189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
491189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
491189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
493431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
494166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
494176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.51ms 
494177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
494177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
494178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
496403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
497140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
497147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
497148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
497148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
497149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
499394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
500135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
500154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.07ms 
500156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
500156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
500156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
502397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
503133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
503154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.87ms 
503156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
503156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
503156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
505399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
506137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
506154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.65ms 
506156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
506156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
506156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
508409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
509147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
509164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms 
509165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
509165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
509166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
511395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
512130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
512148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.27ms 
512149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
512149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
512150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
514375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
515110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
515154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.98ms 
515156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
515156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
515157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
517386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
518120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
518125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
518126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
518126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
518127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
520344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
521078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
521082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
521083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
521083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
521084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
523308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
524041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
524045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
524046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
524046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
524046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
526272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
527007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
527019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.85ms 
527020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
527020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
527021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
529251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
529985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
529991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
529992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
529992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
529993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
532232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
532947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
532949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
532950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
532950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
532951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
535183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
535916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
535925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
535926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
535926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
535927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
538146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
538878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
538887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.24ms 
538888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
538888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
538889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
541111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
541844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
541856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 
541857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
541857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
541858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
544075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
544810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
544812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 891.79ns 
544814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
544814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
544815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
547034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
547769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
547772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
547773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
547773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
547774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
549993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
550726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
550731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
550732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
550733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
550733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
552967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
553699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
553704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
553705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
553705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
553706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
555923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
556659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
556699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.64ms 
556700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
556700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
556701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
558929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
559663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
559679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.03ms 
559680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
559681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
559681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
561903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
562636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
562647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
562648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
562648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
562649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
564895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
565633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
565635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 282.9ns 
565636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
565636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.2ns 
565637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
567867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
568600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
568675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.95ms 
568676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
568677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
568677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
570908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
571644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
571675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.59ms 
571677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
571677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
571677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
573919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
574653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
574655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 224.3ns 
574656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
574656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
574656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
576879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
577613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
577615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 182.2ns 
577616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
577616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
577616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
579834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
580572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
580573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 195.5ns 
580575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
580575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
580575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
582812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
583546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
583547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 320ns 
583549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
583549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
583549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
585766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
586499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
586594     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
586600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99.2ms 
586602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
586602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
586603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
588830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
589563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
589604     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
589605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.03ms 
589606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
589606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
589607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
591850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
592587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
592588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
592612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
592663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
592676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
592681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
592694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
592696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
592697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
592698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
592704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
592704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
592709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
592710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
592937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
592938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
592940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
592941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
592942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
593076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
593077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
593079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
593081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
593082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
593083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
593249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
593251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
593252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
593253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
593254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
593256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
593378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
593379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
593380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
593381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
593381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
593382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
593396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
593396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
593397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
593398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
593399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
593400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
593411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
593412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
593413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
593414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
593415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
593415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
593533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
593534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
593536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
593651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
593653     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)'' 
593654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
593656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
593656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
593657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
593658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
593660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
593664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
593664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
593666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
593667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
593667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
593768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
593771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
593772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
593773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
593774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
593775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
593777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
593906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
593907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
593908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
593909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
593910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
593910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
593911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
593912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
594002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
594003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
594082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
594085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
594090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
594091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
594094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
594095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
594096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
594096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
594096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
594097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
594106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
594113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
594211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
594212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
594214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
594215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
594215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
594216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
594216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
594217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
594261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
594265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
594344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
594345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
594346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
594348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
594349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
594351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
594473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
594477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
594479     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)'' 
594480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
594481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
594482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
594483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
594483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
594491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
594496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
594497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
594498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
594615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
594616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
594617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
594618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
594618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
594619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
594711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
594713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
594714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
594715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
594716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
594716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
594716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
594717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
594799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
594801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
594881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
594881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
594882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
594885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
594888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
594893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
595002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
595002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
595003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
595004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
595015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
595097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
598590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
598591     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)'' 
598595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
598597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
598598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
598598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
598600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
598607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
598607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
598608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
598609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
598610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
598698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
598702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
598703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
598704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
598706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
598706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
598707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
598797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
598798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
598799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
598800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
598801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
598802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
598802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
598803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
598875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
598876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
598946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
598950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
598954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
598954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
598955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
598956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
598965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
599041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
599042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
599043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
599044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
599113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
599124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
599125     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)'' 
599125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
599127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
599127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
599127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
599128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
599138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
599138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
599139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
599141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
599141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
599225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
599226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
599227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
599228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
599229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
599319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
599323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
599324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
599324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
599325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
599325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
599326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
599420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
599420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
599421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
599422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
599423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
599423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
599427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
599428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
599428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
599429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
599430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
599431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
599431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
599432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
599432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
599517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
599518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
599524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
599598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
599678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
599680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
599681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
599681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
599682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
599683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
599683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
599684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
599684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
599765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
599771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
599856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
599857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
599858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
599859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
599859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
599860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
599860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
599860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
599865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
599866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
599941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
599987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
599992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
600084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
600085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
600086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
600086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
600087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
600087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
600087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
600088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
600138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
600139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
600140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
600140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
600141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
600146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
600151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
600259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
600342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
600343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
600343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
600344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
600502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
600585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
600585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
603446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
603450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
603451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
603452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
603453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
603560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
603561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
603562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
603563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
603563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
603662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
606416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
609428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
609432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
609433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
609433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
609434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
609541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
609541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
609542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
609543     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)' ...' 
609544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
610624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
610624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
610625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
613092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
613826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
613828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
613829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
613837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
613846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
613848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
613850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
613852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
613857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
613857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
613862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
613863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
613865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
613875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
613876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
613877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
613926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
613927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
613928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
613928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
613929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
613994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
613995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
613996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
613997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
613997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
614001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
614002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
614002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
614003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
614004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
614005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
614092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
614092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
614093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
614094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
614095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
614095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
614191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
614191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
614192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
614193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
614193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
614194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
614194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
614195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
614196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
614196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
614197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
614197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
614197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
614198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
614198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
614199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
614199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
614200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
614200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
614203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
614239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
614240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
614298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
614299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
614300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
614301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
614302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
614303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
614348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
614351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
614352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
614352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
614354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
614355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
614355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
614400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
614403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
614406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
614464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
614516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
614516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.7ns 
614517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
616730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
617482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
617498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.61ms