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

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
198
tests
failures
ignored
13m24.51s
duration
100%
successful
Tests
Standard output
Tests

Test	Method name	Duration	Result
powPositive	data()[100]	3.904s	passed
powPositiveConcrete	data()[101]	3.941s	passed
powGeq1Concrete	data()[102]	3.885s	passed
pow2InIntLower	data()[103]	3.873s	passed
pow2InIntUpper	data()[104]	3.896s	passed
logSelfConcrete	data()[105]	3.958s	passed
log1Concrete	data()[106]	3.863s	passed
logProduct	data()[107]	3.931s	passed
logTimesBaseConcrete	data()[108]	3.942s	passed
logProdIdentity	data()[109]	3.917s	passed
moduloByteIsInByte	data()[10]	4.005s	passed
logProdIdentityConcrete	data()[110]	3.917s	passed
logPowIdentity	data()[111]	3.887s	passed
logPowIdentityConcrete	data()[112]	3.891s	passed
logPositive	data()[113]	3.873s	passed
logPositiveConcrete	data()[114]	3.935s	passed
logMono	data()[115]	3.989s	passed
logMonoConcrete	data()[116]	3.950s	passed
powLogLess	data()[117]	3.812s	passed
powLogMore2	data()[118]	3.894s	passed
logLessThanPow	data()[119]	3.886s	passed
moduloCharIsInChar	data()[11]	3.916s	passed
logLessThanPowConcrete	data()[120]	3.909s	passed
logSqueeze	data()[121]	3.895s	passed
ifthenelse_equals	data()[122]	3.851s	passed
ifthenelse_equals_1	data()[123]	3.942s	passed
ifthenelse_equals_2	data()[124]	3.857s	passed
disjointWithSingleton1	data()[125]	3.819s	passed
disjointWithSingleton2	data()[126]	3.842s	passed
disjointArrayRanges	data()[127]	3.872s	passed
disjointArrayRangeAllFields1	data()[128]	3.894s	passed
disjointArrayRangeAllFields2	data()[129]	3.842s	passed
div_unique1	data()[12]	3.948s	passed
seqSelfDefinition	data()[130]	3.924s	passed
seqOutsideValue	data()[131]	3.892s	passed
castedGetAny	data()[132]	3.914s	passed
seqGetAlphaCast	data()[133]	3.839s	passed
getOfSeqSingleton	data()[134]	3.897s	passed
getOfSeqSingletonConcrete	data()[135]	3.901s	passed
getOfSeqConcat	data()[136]	3.901s	passed
getOfSeqSub	data()[137]	3.902s	passed
getOfSeqReverse	data()[138]	3.893s	passed
lenOfSeqEmpty	data()[139]	3.938s	passed
div_unique2	data()[13]	4.058s	passed
lenOfSeqSingleton	data()[140]	3.939s	passed
lenOfSeqConcat	data()[141]	3.884s	passed
lenOfSeqSub	data()[142]	3.845s	passed
lenOfSeqReverse	data()[143]	3.872s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.868s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.972s	passed
getOfSeqSingletonEQ	data()[146]	3.946s	passed
getOfSeqConcatEQ	data()[147]	3.924s	passed
getOfSeqSubEQ	data()[148]	3.886s	passed
getOfSeqReverseEQ	data()[149]	3.887s	passed
div_exists	data()[14]	4.170s	passed
lenOfSeqEmptyEQ	data()[150]	3.893s	passed
lenOfSeqSingletonEQ	data()[151]	3.974s	passed
lenOfSeqConcatEQ	data()[152]	3.910s	passed
lenOfSeqSubEQ	data()[153]	3.991s	passed
lenOfSeqReverseEQ	data()[154]	3.941s	passed
getOfSeqDefEQ	data()[155]	3.937s	passed
lenOfSeqDefEQ	data()[156]	3.946s	passed
seqConcatWithSeqEmpty1	data()[157]	3.945s	passed
seqConcatWithSeqEmpty2	data()[158]	3.885s	passed
seqReverseOfSeqEmpty	data()[159]	3.913s	passed
div_one	data()[15]	3.928s	passed
subSeqComplete	data()[160]	3.882s	passed
subSeqTailR	data()[161]	3.940s	passed
subSeqTailL	data()[162]	3.956s	passed
subSeqTailEQR	data()[163]	3.991s	passed
subSeqTailEQL	data()[164]	4.028s	passed
seqDef_split	data()[165]	3.971s	passed
seqDef_induction_upper	data()[166]	4.026s	passed
seqDef_induction_upper_concrete	data()[167]	3.968s	passed
seqDef_induction_lower	data()[168]	3.994s	passed
seqDef_induction_lower_concrete	data()[169]	4.007s	passed
jdiv_one	data()[16]	3.919s	passed
seqDef_split_in_three	data()[170]	4.106s	passed
seqDef_empty	data()[171]	3.961s	passed
seqDef_one_summand	data()[172]	3.947s	passed
seqDef_lower_equals_upper	data()[173]	3.932s	passed
seqDefOfSeq	data()[174]	3.951s	passed
seqSelfDefinitionEQ2	data()[175]	3.932s	passed
indexOfSeqSingleton	data()[176]	3.915s	passed
indexOfSeqConcatFirst	data()[177]	3.923s	passed
indexOfSeqConcatSecond	data()[178]	3.918s	passed
indexOfSeqSub	data()[179]	3.928s	passed
div_zero	data()[17]	3.969s	passed
lenOfArray2seq	data()[180]	3.870s	passed
getAnyOfArray2seq	data()[181]	4.017s	passed
getOfArray2seq	data()[182]	3.853s	passed
getAnyOfNPermInv	data()[183]	3.912s	passed
seqNPermRange	data()[184]	4.055s	passed
seqPermTrans	data()[185]	4.004s	passed
seqPermRefl	data()[186]	3.967s	passed
seqPermSplit	data()[187]	3.927s	passed
seqNPermRight	data()[188]	4.182s	passed
seqPermFromSwap	data()[189]	3.958s	passed
divResZero1	data()[18]	4.009s	passed
seqPermTransAlt0	data()[190]	3.943s	passed
seqPermTransAlt1	data()[191]	3.978s	passed
seqPermTransAlt2	data()[192]	3.886s	passed
seqPermTransAlt3	data()[193]	3.896s	passed
seqPermForall	data()[194]	4.034s	passed
seqPermExists	data()[195]	3.990s	passed
schiffl_lemma_2	data()[196]	29.146s	passed
schiffl_thm_1	data()[197]	4.998s	passed
eqSameSeq	data()[198]	3.962s	passed
divResZero2	data()[19]	3.950s	passed
eqTermCut	data()[1]	4.749s	passed
divResOne1	data()[20]	3.883s	passed
divResOne2	data()[21]	3.919s	passed
div_cancel1	data()[22]	3.879s	passed
div_cancel2	data()[23]	3.858s	passed
divAddMultDenom	data()[24]	3.979s	passed
divMinus	data()[25]	3.955s	passed
divMinusDenom	data()[26]	4.028s	passed
divLeastDPos	data()[27]	3.911s	passed
divLeastDNeg	data()[28]	3.995s	passed
divGreatestDPos	data()[29]	3.943s	passed
equivAllRight	data()[2]	4.379s	passed
divGreatestDNeg	data()[30]	3.976s	passed
divIncreasingPos	data()[31]	4.020s	passed
divIncreasingNeg	data()[32]	3.952s	passed
jdiv_zero	data()[33]	3.893s	passed
jdivPulloutMinusNum	data()[34]	3.909s	passed
jdivPulloutMinusDenom	data()[35]	4.003s	passed
jdiv_uniquePosPos	data()[36]	3.911s	passed
jdiv_uniquePosNeg	data()[37]	3.963s	passed
jdiv_uniqueNegPos	data()[38]	3.851s	passed
jdiv_uniqueNegNeg	data()[39]	3.836s	passed
irrflConcrete1	data()[3]	4.229s	passed
jdivMultDenom1	data()[40]	3.880s	passed
jdivMultDenom2	data()[41]	3.833s	passed
mod_geZero	data()[42]	3.810s	passed
mod_lessDenom	data()[43]	3.868s	passed
jmod_NumPos	data()[44]	3.819s	passed
jmod_NumNeg	data()[45]	3.855s	passed
jmod_geZero	data()[46]	3.813s	passed
jmodNumZero	data()[47]	3.771s	passed
jmod_pulloutminusNum	data()[48]	3.872s	passed
jmod_pulloutminusDenom	data()[49]	3.805s	passed
irrflConcrete2	data()[4]	4.068s	passed
jmodUnique1	data()[50]	3.941s	passed
jmodUnique2	data()[51]	3.909s	passed
intDivRem	data()[52]	3.815s	passed
jmodjmod	data()[53]	4.029s	passed
jmodDivisible	data()[54]	3.868s	passed
jmodDivisibleRep	data()[55]	3.786s	passed
jdivAddMultDenom	data()[56]	4.027s	passed
jmodAltZero	data()[57]	3.789s	passed
jmodAddMultDenomZero	data()[58]	3.755s	passed
polyDiv_zero	data()[59]	3.820s	passed
cancel_gtPos	data()[5]	4.135s	passed
polyMod_ltdivDenom	data()[60]	3.848s	passed
bsum_empty	data()[61]	3.812s	passed
bsum_induction_upper	data()[62]	3.831s	passed
bsum_induction_lower	data()[63]	3.811s	passed
bsum_num_of_bounds	data()[64]	3.864s	passed
bsum_num_of_bounds2	data()[65]	3.785s	passed
bsum_induction_upper2	data()[66]	3.870s	passed
bsum_induction_upper_concrete	data()[67]	3.762s	passed
bsum_induction_upper_concrete_2	data()[68]	3.766s	passed
bsum_induction_upper2_concrete	data()[69]	3.810s	passed
cancel_gtNeg	data()[6]	4.018s	passed
bsum_induction_lower_concrete	data()[70]	3.845s	passed
bsum_induction_lower2	data()[71]	3.782s	passed
bsum_induction_lower2_concrete	data()[72]	3.844s	passed
bsum_positive	data()[73]	3.925s	passed
bsum_upper_bound	data()[74]	4.014s	passed
bsum_lower_bound	data()[75]	4.033s	passed
bsum_positive_lower_bound_element	data()[76]	3.990s	passed
bsum_sub_same_index	data()[77]	3.954s	passed
bsum_less_same_index	data()[78]	4.016s	passed
bsum_equal_except_one_index	data()[79]	3.887s	passed
moduloIntIsInInt	data()[7]	4.109s	passed
bsum_num_of_is_max	data()[80]	3.926s	passed
bsum_num_of_is_max2	data()[81]	3.897s	passed
bsum_num_of_is_max3	data()[82]	4.030s	passed
bsum_num_of_is_max4	data()[83]	4.045s	passed
bsum_num_of_lt_max	data()[84]	3.970s	passed
bsum_num_of_lt_max2	data()[85]	4.024s	passed
bsum_num_of_lt_max3	data()[86]	4.007s	passed
bsum_num_of_lt_max4	data()[87]	3.917s	passed
bsum_num_of_gt0	data()[88]	3.899s	passed
bsum_num_of_gt0_alt	data()[89]	3.953s	passed
moduloLongIsInLong	data()[8]	3.945s	passed
bsum_add_concrete	data()[90]	3.873s	passed
bprod_all_positive	data()[91]	3.905s	passed
bprod_split	data()[92]	3.972s	passed
powConcrete0	data()[93]	3.916s	passed
powConcrete1	data()[94]	3.884s	passed
powSplitFactor	data()[95]	3.903s	passed
powAdd	data()[96]	3.930s	passed
powMono	data()[97]	3.928s	passed
powMonoConcrete	data()[98]	3.914s	passed
powMonoConcreteRight	data()[99]	3.967s	passed
moduloShortIsInShort	data()[9]	3.889s	passed
Standard output

411        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
442        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 15.65ms 
776        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
799        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)

2219       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2221       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2226       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2226       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4617       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10932      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.16s 
11033      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11083      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.1ns 
11103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11105      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.91ms 
11114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14637      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
14640      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15837      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.09ms 
15856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15857      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 467.62ns 
15859      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
19138      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20232      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.57ms 
20245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 459.02ns 
20247      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23401      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
23402      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24452      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24472      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.03ms 
24482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24489      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.53ms 
24500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27553      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
27553      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
28539      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
28546      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
28549      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
28549      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.12ns 
28551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31569      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
31570      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
32582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
32681      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.76ms 
32683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
32683      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.71ns 
32684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
35665      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
36675      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
36698      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.36ms 
36702      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
36703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 423.61ns 
36704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39804      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
39805      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
40804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
40808      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 761.24ns 
40811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
40812      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 492.52ns 
40813      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43792      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
43792      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
44750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
44754      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.23ns 
44757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
44757      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.72ns 
44759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
47724      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
48641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
48644      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 593.63ns 
48645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
48645      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.31ns 
48646      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51707      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
51707      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
52644      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
52647      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 690.03ns 
52650      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
52651      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.71ns 
52652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55573      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
55574      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
56560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
56563      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 724.13ns 
56567      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
56568      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.22ns 
56569      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59502      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
59503      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
60452      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
60512      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.96ms 
60522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
60530      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.21ns 
60531      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63523      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
63523      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
64469      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
64571      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.65ms 
64573      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
64574      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.71ns 
64582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67540      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
67540      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
68487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
68740      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 242.97ms 
68743      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
68744      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.01ns 
68745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71725      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
71726      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
72660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
72668      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
72679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
72679      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.62ns 
72681      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75608      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
75611      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
76584      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
76589      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
76591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
76594      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.34ms 
76595      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79574      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
79577      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
80505      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
80558      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.21ms 
80560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
80560      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.52ns 
80562      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83559      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
83559      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
84545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
84567      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.89ms 
84569      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
84570      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.32ns 
84571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
87523      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
88495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
88517      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.51ms 
88519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
88519      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.91ns 
88520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91424      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
91424      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
92376      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
92400      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.41ms 
92402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
92402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.4ns 
92403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95334      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
95335      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
96298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
96318      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.25ms 
96322      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
96322      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.72ns 
96324      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99227      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
99227      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
100165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
100198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.21ms 
100200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
100200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.71ns 
100201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
103094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
104052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
104056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
104057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
104057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
104059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
107020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
107974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
108034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.29ms 
108037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
108037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.61ns 
108038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
110968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
111899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
111985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.66ms 
111993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
111994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.91ns 
111995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
114944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
115923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
116019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.37ms 
116025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
116028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.84ms 
116030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
118963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
119920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
119932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.53ms 
119934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
119935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.51ns 
119936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
122993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
123909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
123927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.47ms 
123929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
123929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
123930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
126894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
127848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
127870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.32ms 
127872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
127872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.41ns 
127873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
130863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
131836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
131847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.98ms 
131848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
131848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
131849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
134897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
135856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
135867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.51ms 
135868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
135868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
135869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
138859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
139808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
139818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.39ms 
139820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
139820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.31ns 
139821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
142772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
143705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
143711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
143713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
143713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.9ns 
143714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
146659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
147606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
147620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.77ms 
147622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
147622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.6ns 
147623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
150598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
151537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
151623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.94ms 
151625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
151625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
151626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
154607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
155510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
155534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.44ms 
155536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
155536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.8ns 
155537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
158484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
159468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
159496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.96ms 
159499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
159499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.61ns 
159501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
162390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
163321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
163348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.51ms 
163350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
163350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.1ns 
163351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
166236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
167161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
167184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.92ms 
167186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
167186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
167187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
170071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
171005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
171064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.52ms 
171066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
171066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.41ns 
171067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
173996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
174893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
174897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
174899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
174899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.81ns 
174900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
177774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
178702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
178707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
178709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
178709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
178710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
181617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
182564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
182575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.04ms 
182577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
182577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
182578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
185468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
186384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
186395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
186396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
186396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
186397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
189277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
190223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
190249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.98ms 
190250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
190251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
190251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
193125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
194051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
194063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
194064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
194065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.31ns 
194065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
196910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
197829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
197833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
197836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
197836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.51ns 
197837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
200781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
201701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
201705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
201707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
201707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
201708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
204627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
205504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
205510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
205513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
205513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.01ns 
205514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
208368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
209309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
209450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 126.11ms 
209456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
209458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.57ms 
209459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
212317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
213232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
213363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.63ms 
213366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
213366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.31ns 
213368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
216255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
217173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
217178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
217181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
217181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.61ns 
217182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
220189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
221154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
221208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.32ms 
221210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
221210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.11ns 
221211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
224087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
225035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
225076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.9ms 
225078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
225078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
225079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
227933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
228859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
228862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
228864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
228865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.71ns 
228866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
231739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
232660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
232888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 216.43ms 
232890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
232891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
232891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
235757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
236663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
236678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ms 
236680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
236680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
236681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
239507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
240423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
240433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.97ms 
240435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
240435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
240436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
243307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
244226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
244254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.92ms 
244255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
244255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
244256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
247189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
248085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
248101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
248103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
248103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
248104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
250999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
251908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
251913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
251914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
251914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
251915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
254800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
255738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
255744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
255746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
255746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
255747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
258587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
259522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
259555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.63ms 
259557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
259557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
259557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
262458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
263393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
263419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.93ms 
263421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
263421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.8ns 
263422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
266275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
267182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
267204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.73ms 
267206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
267206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
267207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
270121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
271070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
271074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
271076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
271076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
271077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
273928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
274830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
274836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
274838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
274838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 
274839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
277699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
278595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
278602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
278603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
278603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
278604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
281479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
282408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
282412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
282414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
282415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 463.82ns 
282416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
285329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
286254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
286257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 904.13ns 
286258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
286258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
286259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
289101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
290035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
290040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
290041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
290041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns 
290042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
292948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
293880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
293883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
293885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
293885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
293886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
296793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
297733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
297808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.66ms 
297811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
297811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.61ns 
297812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
300751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
301755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
301822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.21ms 
301823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
301823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
301824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
304833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
305800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
305854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.39ms 
305856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
305856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
305857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
308825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
309764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
309845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.26ms 
309847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
309847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
309848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
312798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
313748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
313799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.99ms 
313800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
313801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 419.11ns 
313802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
316785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
317727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
317814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.57ms 
317816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
317816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
317817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
320751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
321658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
321702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.92ms 
321704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
321704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.51ns 
321705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
324664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
325596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
325628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.08ms 
325629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
325629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
325630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
328530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
329487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
329524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.29ms 
329527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
329527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.11ns 
329528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
332543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
333514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
333555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.2ms 
333557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
333557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
333558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
336601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
337558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
337600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.47ms 
337602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
337602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
337603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
340575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
341529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
341570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.11ms 
341572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
341573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.71ns 
341574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
344496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
345557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
345594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.89ms 
345603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
345603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.81ns 
345604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
348608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
349564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
349601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.34ms 
349602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
349603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
349603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
352559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
353488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
353518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.95ms 
353520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
353520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
353521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
356431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
357369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
357416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.35ms 
357419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
357420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 589.61ns 
357421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
360391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
361332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
361370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.98ms 
361371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
361371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
361372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
364290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
365233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
365243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.74ms 
365245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
365245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
365246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
368179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
369124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
369149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.07ms 
369150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
369150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
369151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
372158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
373115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
373120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
373122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
373123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.41ns 
373123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
376084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
377034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
377037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 723.32ns 
377038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
377038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
377039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
379963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
380917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
380920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
380922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
380922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.11ns 
380923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
383875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
384813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
384823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.87ms 
384824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
384824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.11ns 
384825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
387804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
388744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
388754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.43ms 
388755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
388755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.62ns 
388756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
391713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
392664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
392681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.59ms 
392683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
392683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
392684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
395656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
396591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
396595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
396597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
396597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
396597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
399582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
400560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
400562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 676.93ns 
400564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
400564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
400565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
403519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
404456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
404466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms 
404469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
404469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.02ns 
404470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
407442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
408405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
408407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 894.25ns 
408409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
408409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
408409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
411335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
412289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
412292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
412293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
412293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
412294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
415217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
416163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
416165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 766.14ns 
416167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
416167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
416168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
419118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
420056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
420061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
420062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
420063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.91ns 
420063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
423056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
424007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
424019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.46ms 
424020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
424021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.11ns 
424021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
426941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
427875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
427882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
427883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
427884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
427884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
430855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
431804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
431813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
431815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
431815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
431815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
434779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
435750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
435755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
435756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
435756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
435757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
438701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
439650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
439672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.54ms 
439674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
439674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
439675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
442650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
443584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
443589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
443591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
443591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
443591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
446526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
447472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
447476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
447478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
447478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.71ns 
447479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
450413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
451361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
451367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
451368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
451369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
451369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
454275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
455216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
455241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.63ms 
455242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
455242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
455243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
458203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
459169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
459174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.52ns 
459176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
459176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
459177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
462157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
463098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
463163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.61ms 
463166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
463166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.31ns 
463167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
466156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
467111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
467115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
467117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
467117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
467118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
469960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
470895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
470927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.24ms 
470929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
470929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
470929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
473835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
474793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
474822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.42ms 
474823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
474823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
474824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
477713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
478672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
478707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.15ms 
478709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
478709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
478710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
481657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
482613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
482616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 789.04ns 
482620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
482620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.51ns 
482623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
485556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
486504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
486512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
486513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
486513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
486514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
489411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
490358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
490362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
490364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
490364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.51ns 
490365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
493362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
494301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
494305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
494306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
494306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
494307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
497209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
498158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
498161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
498163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
498163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
498163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
501031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
501976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
501980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
501981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
501981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
501982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
504859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
505819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
505823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
505824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
505824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
505825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
508734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
509679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
509694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.25ms 
509699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
509699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
509700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
512624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
513576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
513591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.34ms 
513593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
513593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
513594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
516472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
517419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
517433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.49ms 
517435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
517435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
517436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
520365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
521340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
521357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms 
521359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
521359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns 
521360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
524249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
525226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
525249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.89ms 
525251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
525252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.61ns 
525253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
528192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
529155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
529163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms 
529164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
529164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
529165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
532050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
533000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
533002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.23ns 
533004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
533004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.31ns 
533005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
535940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
536895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
536899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
536900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
536901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
536901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
539828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
540797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
540800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
540801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
540801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
540802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
543732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
544685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
544701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.82ms 
544702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
544702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
544703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
547638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
548597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
548603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
548605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
548605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
548606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
551520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
552486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
552496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
552497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
552497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
552498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
555465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
556431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
556434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 947.02ns 
556435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
556435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
556436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
559409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
560370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
560373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 908.04ns 
560374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
560374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
560375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
563290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
564252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
564257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
564259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
564259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.91ns 
564260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
567143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
568099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
568103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
568104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
568104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
568105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
571024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
571971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
571975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
571976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
571976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
571977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
574893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
575838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
575842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
575844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
575844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
575845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
578844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
579806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
579814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
579815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
579815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
579816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
582792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
583756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
583760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
583761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
583761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
583762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
586706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
587670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
587685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.46ms 
587686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
587686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
587687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
590614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
591568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
591571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 904.63ns 
591572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
591572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
591573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
594498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
595448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
595457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.36ms 
595459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
595459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
595460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
598396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
599347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
599350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
599352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
599352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
599352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
602342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
603321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
603324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
603331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
603331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.41ns 
603332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
606255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
607227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
607234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.36ms 
607236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
607236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
607236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
610261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
611221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
611225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
611227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
611227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
611227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
614206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
615161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
615166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
615167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
615167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
615168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
618104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
619099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
619104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
619105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
619105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
619106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
622057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
623042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
623050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
623051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
623051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
623052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
625980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
626974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
626994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.47ms 
626996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
626996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.21ns 
626997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
629914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
630854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
630879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.99ms 
630881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
630881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
630881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
633808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
634778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
634793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.19ms 
634794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
634794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
634795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
637703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
638659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
638674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.39ms 
638676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
638676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.41ns 
638678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
641612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
642579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
642614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.22ms 
642616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
642616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
642617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
645558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
646535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
646570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.36ms 
646571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
646571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
646572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
649524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
650528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
650561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.99ms 
650562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
650562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
650563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
653600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
654569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
654589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.56ms 
654591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
654591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
654592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
657553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
658518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
658560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.38ms 
658561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
658562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
658562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
661529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
662521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
662586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.08ms 
662588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
662588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
662589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
665528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
666491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
666554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.42ms 
666556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
666556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
666557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
669502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
670492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
670548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.57ms 
670550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
670550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
670551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
673533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
674493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
674555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.74ms 
674556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
674556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
674557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
677494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
678503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
678661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 150.68ms 
678663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
678663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
678664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
681638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
682611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
682622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.36ms 
682624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
682624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
682624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
685596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
686557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
686569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.06ms 
686571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
686571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.31ns 
686572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
689529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
690493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
690501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
690502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
690502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
690503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
693465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
694426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
694452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.59ms 
694455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
694455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
694456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
697385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
698368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
698384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
698386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
698386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
698387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
701341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
702294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
702299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
702301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
702301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
702301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
705235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
706198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
706222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.53ms 
706224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
706224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
706225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
709159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
710118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
710140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.31ms 
710141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
710141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
710142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
713076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
714040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
714068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.13ms 
714071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
714071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.41ns 
714072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
716974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
717934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
717938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
717939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
717940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
717940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
720924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
721950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
721955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
721957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
721957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
721957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
724847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
725800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
725808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
725809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
725809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
725810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
728744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
729711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
729721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms 
729722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
729722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
729723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
732661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
733674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
733775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.97ms 
733777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
733777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
733777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
736754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
737739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
737779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.21ms 
737781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
737781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
737782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
740735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
741716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
741747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.12ms 
741748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
741748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
741749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
744705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
745671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
745674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 338.31ns 
745675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
745675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
745676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
748595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
749552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
749855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 290.63ms 
749858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
749858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.41ns 
749859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
752776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
753743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
753813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.51ms 
753815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
753815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
753816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
756769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
757754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
757757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 492.01ns 
757758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
757758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
757759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
760759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
761732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
761735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 464.72ns 
761736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
761736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
761737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
764656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
765618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
765620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 438.61ns 
765622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
765622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
765622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
768539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
769514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
769516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.42ns 
769518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
769518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
769518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
772419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
772419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
773382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
773525     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
773549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 164.25ms 
773553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
773553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.41ns 
773554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
776512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
777475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
777540     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
777541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.08ms 
777543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
777543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.9ns 
777545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
780476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
781441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
781443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ns 
781478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
781525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
781548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
781563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
781571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
781577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
781579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
781582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
781586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
781588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
781591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
781592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
781857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
781860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
781862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
781864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
781865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
782051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
782052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
782056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
782058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
782060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
782060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
782329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
782332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
782333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
782334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
782336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
782339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
782552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
782554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
782555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
782556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
782557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
782558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
782565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
782566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
782567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
782569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
782571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
782573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
782580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
782581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
782582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
782583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
782584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
782585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
782740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
782741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
782742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
782886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
782888     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)'' 
782890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
782892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
782892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
782893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
782894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
782895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
782903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
782905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
782907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
782907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
782908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
783044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
783048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
783050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
783051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
783052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
783053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
783060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
783198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
783200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
783201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
783203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
783203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
783204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
783205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
783207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
783321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
783323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
783450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
783455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
783460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
783462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
783462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
783464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
783465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
783465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
783466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
783467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
783477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
783482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
783596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
783598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
783599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
783600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
783601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
783602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
783602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
783603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
783663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
783669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
783778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
783780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
783782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
783784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
783785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
783786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
783957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
783962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
783965     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)'' 
783968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
783972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
783977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
783978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
783979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
783992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
784003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
784005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
784006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
784143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
784145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
784147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
784150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
784152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
784153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
784283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
784286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
784287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
784289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
784290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
784291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
784292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
784293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
784405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
784407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
784519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
784520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
784521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
784532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
784537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
784542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
784701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
784702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
784703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
784705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
784718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
784825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
789478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
789479     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)'' 
789486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
789488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
789488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
789489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
789490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
789500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
789502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
789504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
789504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
789505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
789627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
789632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
789633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
789634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
789635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
789636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
789637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
789817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
789818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
789819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
789821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
789821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
789822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
789823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
789825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
789929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
789931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
790022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
790027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
790033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
790034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
790035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
790036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
790049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
790150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
790152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
790153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
790154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
790245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
790258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
790259     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)'' 
790261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
790262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
790263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
790264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
790264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
790278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
790280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
790282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
790282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
790283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
790395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
790398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
790399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
790400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
790401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
790520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
790526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
790528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
790529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
790530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
790530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
790531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
790657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
790659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
790660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
790662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
790662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
790663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
790664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
790665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
790666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
790667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
790669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
790669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
790670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
790670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
790672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
790790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
790792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
790800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
790909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
791017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
791019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
791020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
791021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
791022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
791022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
791023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
791023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
791024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
791136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
791143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
791264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
791265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
791266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
791267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
791267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
791268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
791268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
791269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
791276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
791277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
791381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
791388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
791396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
791532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
791534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
791535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
791536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
791536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
791537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
791537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
791538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
791619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
791621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
791621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
791622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
791623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
791685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
791691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
791837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
791952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
791953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
791954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
791955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
792165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
792277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
792278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
796232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
796238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
796239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
796240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
796240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
796385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
796386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
796387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
796388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
796389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
796521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
800757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
805060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
805066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
805067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
805068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
805069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
805218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
805220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
805221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
805222     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)' ...' 
805225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
806689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
806689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.81ns 
806690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
809769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
809769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
810703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
810704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
810705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
810712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
810726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
810729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
810731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
810732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
810737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
810738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
810742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
810745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
810745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
810756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
810759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
810759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
810821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
810823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
810823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
810824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
810824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
810916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
810917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
810920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
810921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
810921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
810926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
810926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
810927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
810928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
810929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
810930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
811048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
811049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
811050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
811051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
811052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
811053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
811175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
811176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
811177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
811177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
811178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
811179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
811180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
811180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
811182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
811182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
811183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
811184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
811184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
811185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
811186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
811186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
811187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
811188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
811189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
811194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
811246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
811247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
811331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
811333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
811335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
811336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
811337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
811338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
811413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
811416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
811417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
811419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
811421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
811421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
811422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
811490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
811493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
811497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
811578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
811688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
811688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.31ns 
811689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
814592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
814592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
815604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
815647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.73ms