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

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

Test	Method name	Duration	Result
powPositive	data()[100]	3.620s	passed
powPositiveConcrete	data()[101]	3.591s	passed
powGeq1Concrete	data()[102]	3.587s	passed
pow2InIntLower	data()[103]	3.652s	passed
pow2InIntUpper	data()[104]	3.602s	passed
logSelfConcrete	data()[105]	3.630s	passed
log1Concrete	data()[106]	3.680s	passed
logProduct	data()[107]	3.639s	passed
logTimesBaseConcrete	data()[108]	3.611s	passed
logProdIdentity	data()[109]	3.679s	passed
moduloByteIsInByte	data()[10]	3.791s	passed
logProdIdentityConcrete	data()[110]	3.619s	passed
logPowIdentity	data()[111]	3.646s	passed
logPowIdentityConcrete	data()[112]	3.637s	passed
logPositive	data()[113]	3.661s	passed
logPositiveConcrete	data()[114]	3.632s	passed
logMono	data()[115]	3.673s	passed
logMonoConcrete	data()[116]	3.659s	passed
powLogLess	data()[117]	3.632s	passed
powLogMore2	data()[118]	3.663s	passed
logLessThanPow	data()[119]	3.716s	passed
moduloCharIsInChar	data()[11]	3.736s	passed
logLessThanPowConcrete	data()[120]	3.710s	passed
logSqueeze	data()[121]	3.658s	passed
ifthenelse_equals	data()[122]	3.709s	passed
ifthenelse_equals_1	data()[123]	3.679s	passed
ifthenelse_equals_2	data()[124]	3.648s	passed
disjointWithSingleton1	data()[125]	3.678s	passed
disjointWithSingleton2	data()[126]	3.658s	passed
disjointArrayRanges	data()[127]	3.675s	passed
disjointArrayRangeAllFields1	data()[128]	3.567s	passed
disjointArrayRangeAllFields2	data()[129]	3.660s	passed
div_unique1	data()[12]	3.871s	passed
seqSelfDefinition	data()[130]	3.741s	passed
seqOutsideValue	data()[131]	3.678s	passed
castedGetAny	data()[132]	3.659s	passed
seqGetAlphaCast	data()[133]	3.661s	passed
getOfSeqSingleton	data()[134]	3.644s	passed
getOfSeqSingletonConcrete	data()[135]	3.618s	passed
getOfSeqConcat	data()[136]	3.651s	passed
getOfSeqSub	data()[137]	3.653s	passed
getOfSeqReverse	data()[138]	3.656s	passed
lenOfSeqEmpty	data()[139]	3.685s	passed
div_unique2	data()[13]	3.798s	passed
lenOfSeqSingleton	data()[140]	3.681s	passed
lenOfSeqConcat	data()[141]	3.680s	passed
lenOfSeqSub	data()[142]	3.720s	passed
lenOfSeqReverse	data()[143]	3.701s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.638s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.725s	passed
getOfSeqSingletonEQ	data()[146]	3.710s	passed
getOfSeqConcatEQ	data()[147]	3.662s	passed
getOfSeqSubEQ	data()[148]	3.745s	passed
getOfSeqReverseEQ	data()[149]	3.720s	passed
div_exists	data()[14]	3.837s	passed
lenOfSeqEmptyEQ	data()[150]	3.657s	passed
lenOfSeqSingletonEQ	data()[151]	3.717s	passed
lenOfSeqConcatEQ	data()[152]	3.680s	passed
lenOfSeqSubEQ	data()[153]	3.675s	passed
lenOfSeqReverseEQ	data()[154]	3.732s	passed
getOfSeqDefEQ	data()[155]	3.708s	passed
lenOfSeqDefEQ	data()[156]	3.682s	passed
seqConcatWithSeqEmpty1	data()[157]	3.681s	passed
seqConcatWithSeqEmpty2	data()[158]	3.718s	passed
seqReverseOfSeqEmpty	data()[159]	3.713s	passed
div_one	data()[15]	3.800s	passed
subSeqComplete	data()[160]	3.684s	passed
subSeqTailR	data()[161]	3.710s	passed
subSeqTailL	data()[162]	3.739s	passed
subSeqTailEQR	data()[163]	3.793s	passed
subSeqTailEQL	data()[164]	3.730s	passed
seqDef_split	data()[165]	3.723s	passed
seqDef_induction_upper	data()[166]	3.796s	passed
seqDef_induction_upper_concrete	data()[167]	3.702s	passed
seqDef_induction_lower	data()[168]	3.739s	passed
seqDef_induction_lower_concrete	data()[169]	3.695s	passed
jdiv_one	data()[16]	3.757s	passed
seqDef_split_in_three	data()[170]	3.741s	passed
seqDef_empty	data()[171]	3.746s	passed
seqDef_one_summand	data()[172]	3.716s	passed
seqDef_lower_equals_upper	data()[173]	3.798s	passed
seqDefOfSeq	data()[174]	3.754s	passed
seqSelfDefinitionEQ2	data()[175]	3.763s	passed
indexOfSeqSingleton	data()[176]	3.676s	passed
indexOfSeqConcatFirst	data()[177]	3.737s	passed
indexOfSeqConcatSecond	data()[178]	3.762s	passed
indexOfSeqSub	data()[179]	3.728s	passed
div_zero	data()[17]	3.860s	passed
lenOfArray2seq	data()[180]	3.736s	passed
getAnyOfArray2seq	data()[181]	3.760s	passed
getOfArray2seq	data()[182]	3.759s	passed
getAnyOfNPermInv	data()[183]	3.697s	passed
seqNPermRange	data()[184]	3.727s	passed
seqPermTrans	data()[185]	3.713s	passed
seqPermRefl	data()[186]	3.772s	passed
seqPermSplit	data()[187]	3.703s	passed
seqNPermRight	data()[188]	3.839s	passed
seqPermFromSwap	data()[189]	3.726s	passed
divResZero1	data()[18]	3.740s	passed
seqPermTransAlt0	data()[190]	3.677s	passed
seqPermTransAlt1	data()[191]	3.744s	passed
seqPermTransAlt2	data()[192]	3.648s	passed
seqPermTransAlt3	data()[193]	3.665s	passed
seqPermForall	data()[194]	3.847s	passed
seqPermExists	data()[195]	3.876s	passed
schiffl_lemma_2	data()[196]	27.106s	passed
schiffl_thm_1	data()[197]	4.704s	passed
eqSameSeq	data()[198]	3.984s	passed
divResZero2	data()[19]	3.724s	passed
eqTermCut	data()[1]	4.679s	passed
divResOne1	data()[20]	3.739s	passed
divResOne2	data()[21]	3.726s	passed
div_cancel1	data()[22]	3.707s	passed
div_cancel2	data()[23]	3.676s	passed
divAddMultDenom	data()[24]	3.791s	passed
divMinus	data()[25]	3.873s	passed
divMinusDenom	data()[26]	3.811s	passed
divLeastDPos	data()[27]	3.694s	passed
divLeastDNeg	data()[28]	3.781s	passed
divGreatestDPos	data()[29]	3.718s	passed
equivAllRight	data()[2]	4.352s	passed
divGreatestDNeg	data()[30]	3.634s	passed
divIncreasingPos	data()[31]	3.722s	passed
divIncreasingNeg	data()[32]	3.777s	passed
jdiv_zero	data()[33]	3.859s	passed
jdivPulloutMinusNum	data()[34]	3.769s	passed
jdivPulloutMinusDenom	data()[35]	3.826s	passed
jdiv_uniquePosPos	data()[36]	3.754s	passed
jdiv_uniquePosNeg	data()[37]	3.768s	passed
jdiv_uniqueNegPos	data()[38]	3.715s	passed
jdiv_uniqueNegNeg	data()[39]	3.732s	passed
irrflConcrete1	data()[3]	4.146s	passed
jdivMultDenom1	data()[40]	3.775s	passed
jdivMultDenom2	data()[41]	3.683s	passed
mod_geZero	data()[42]	3.716s	passed
mod_lessDenom	data()[43]	3.738s	passed
jmod_NumPos	data()[44]	3.743s	passed
jmod_NumNeg	data()[45]	3.738s	passed
jmod_geZero	data()[46]	3.688s	passed
jmodNumZero	data()[47]	3.702s	passed
jmod_pulloutminusNum	data()[48]	3.716s	passed
jmod_pulloutminusDenom	data()[49]	3.745s	passed
irrflConcrete2	data()[4]	3.941s	passed
jmodUnique1	data()[50]	3.742s	passed
jmodUnique2	data()[51]	3.741s	passed
intDivRem	data()[52]	3.610s	passed
jmodjmod	data()[53]	3.672s	passed
jmodDivisible	data()[54]	3.721s	passed
jmodDivisibleRep	data()[55]	3.614s	passed
jdivAddMultDenom	data()[56]	3.824s	passed
jmodAltZero	data()[57]	3.760s	passed
jmodAddMultDenomZero	data()[58]	3.663s	passed
polyDiv_zero	data()[59]	3.688s	passed
cancel_gtPos	data()[5]	3.982s	passed
polyMod_ltdivDenom	data()[60]	3.669s	passed
bsum_empty	data()[61]	3.614s	passed
bsum_induction_upper	data()[62]	3.602s	passed
bsum_induction_lower	data()[63]	3.658s	passed
bsum_num_of_bounds	data()[64]	3.765s	passed
bsum_num_of_bounds2	data()[65]	3.729s	passed
bsum_induction_upper2	data()[66]	3.743s	passed
bsum_induction_upper_concrete	data()[67]	3.622s	passed
bsum_induction_upper_concrete_2	data()[68]	3.578s	passed
bsum_induction_upper2_concrete	data()[69]	3.596s	passed
cancel_gtNeg	data()[6]	3.923s	passed
bsum_induction_lower_concrete	data()[70]	3.619s	passed
bsum_induction_lower2	data()[71]	3.615s	passed
bsum_induction_lower2_concrete	data()[72]	3.592s	passed
bsum_positive	data()[73]	3.702s	passed
bsum_upper_bound	data()[74]	3.726s	passed
bsum_lower_bound	data()[75]	3.669s	passed
bsum_positive_lower_bound_element	data()[76]	3.709s	passed
bsum_sub_same_index	data()[77]	3.657s	passed
bsum_less_same_index	data()[78]	3.690s	passed
bsum_equal_except_one_index	data()[79]	3.598s	passed
moduloIntIsInInt	data()[7]	3.803s	passed
bsum_num_of_is_max	data()[80]	3.702s	passed
bsum_num_of_is_max2	data()[81]	3.642s	passed
bsum_num_of_is_max3	data()[82]	3.705s	passed
bsum_num_of_is_max4	data()[83]	3.680s	passed
bsum_num_of_lt_max	data()[84]	3.647s	passed
bsum_num_of_lt_max2	data()[85]	3.661s	passed
bsum_num_of_lt_max3	data()[86]	3.700s	passed
bsum_num_of_lt_max4	data()[87]	3.635s	passed
bsum_num_of_gt0	data()[88]	3.740s	passed
bsum_num_of_gt0_alt	data()[89]	3.638s	passed
moduloLongIsInLong	data()[8]	3.947s	passed
bsum_add_concrete	data()[90]	3.688s	passed
bprod_all_positive	data()[91]	3.622s	passed
bprod_split	data()[92]	3.636s	passed
powConcrete0	data()[93]	3.620s	passed
powConcrete1	data()[94]	3.588s	passed
powSplitFactor	data()[95]	3.604s	passed
powAdd	data()[96]	3.646s	passed
powMono	data()[97]	3.690s	passed
powMonoConcrete	data()[98]	3.630s	passed
powMonoConcreteRight	data()[99]	3.591s	passed
moduloShortIsInShort	data()[9]	3.914s	passed
Standard output

656        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
701        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 23.66ms 
1081       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1100       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)

2296       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2299       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2302       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2303       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4235       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10714      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.63s 
10813      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10863      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.7ns 
10878      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10880      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.65ms 
10887      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14406      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
14409      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15549      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.61ms 
15564      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 575.23ns 
15566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18853      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
18861      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
19897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19912      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms 
19916      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 499.82ns 
19918      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23081      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
23083      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24052      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24060      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
24063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24063      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.92ns 
24064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27060      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
27061      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
27994      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
28001      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
28004      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
28005      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.43ms 
28007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30973      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
30974      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
31906      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
31980      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.82ms 
31987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
31988      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 599.13ns 
31989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34896      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
34897      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
35853      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
35904      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.57ms 
35910      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
35911      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.01ns 
35912      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
38779      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
39708      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
39711      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 776.33ns 
39714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
39714      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.51ns 
39722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42668      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
42669      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
43654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
43658      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.73ns 
43669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
43670      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.72ns 
43671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46647      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
46648      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
47568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
47571      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 597.42ns 
47575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
47575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.62ns 
47576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
50415      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
51359      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
51363      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 614.53ns 
51366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
51367      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.47ms 
51369      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54195      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
54196      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
55096      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
55099      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 826.34ns 
55101      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
55101      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.21ns 
55102      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57952      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
57953      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
58856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
58970      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 110.17ms 
58972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
58973      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
58977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61821      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
61821      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
62729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
62767      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.26ms 
62772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
62772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 551.42ns 
62774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65538      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
65538      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
66446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
66604      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 147.94ms 
66610      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
66610      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.21ns 
66611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69451      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
69451      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
70401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
70408      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.01ms 
70411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
70411      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 432.22ns 
70413      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73231      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
73232      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
74156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
74166      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ms 
74169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
74169      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.32ns 
74171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77064      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
77065      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
77973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
78026      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.15ms 
78029      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
78029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.72ns 
78031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
80856      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
81746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
81766      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.49ms 
81769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
81770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 565.32ns 
81771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84561      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
84561      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
85473      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
85490      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.22ms 
85492      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
85492      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
85493      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88303      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
88304      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
89211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
89230      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.72ms 
89232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
89232      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118ns 
89233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
92030      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
92937      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
92956      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.43ms 
92958      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
92958      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
92959      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95747      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
95747      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
96637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
96663      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.51ms 
96664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
96664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.11ns 
96665      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99422      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
99423      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
100334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
100338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
100341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
100341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.61ns 
100343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
103122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
104064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
104130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.44ms 
104133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
104133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.52ns 
104134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
107021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
107931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
108002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.7ms 
108005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
108006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.71ns 
108007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
110858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
111756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
111814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.9ms 
111816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
111816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
111817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
114604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
115499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
115509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
115510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
115510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
115511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
118343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
119273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
119289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.68ms 
119291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
119291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
119292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
122103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
122995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
123008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.55ms 
123009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
123010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 473.72ns 
123011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
125741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
126632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
126641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.78ms 
126642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
126643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
126643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
129440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
130354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
130363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.34ms 
130364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
130365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.61ns 
130365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
133192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
134130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
134140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.54ms 
134142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
134142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.71ns 
134143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
137096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
137994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
137999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
138001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
138002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 706.03ns 
138003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
140841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
141735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
141767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.6ms 
141771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
141771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.12ns 
141776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
144627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
145534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
145593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.33ms 
145596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
145596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.61ns 
145597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
148418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
149325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
149348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.72ms 
149349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
149349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
149350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
152176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
153090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
153115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.05ms 
153118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
153118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.11ns 
153119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
155897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
156805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
156831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.75ms 
156833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
156834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.21ns 
156835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
159615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
160539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
160563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.88ms 
160565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
160565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
160566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
163388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
164293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
164338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.96ms 
164340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
164340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
164340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
167148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
168018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
168021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
168023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
168023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
168024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
170847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
171732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
171737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
171738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
171738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
171739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
174556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
175467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
175476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.72ms 
175477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
175477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
175478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
178306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
179209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
179218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.99ms 
179220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
179220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
179221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
182031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
182933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
182957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.73ms 
182958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
182958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
182959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
185666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
186635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
186644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.13ms 
186646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
186646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
186647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
189412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
190340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
190345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
190348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
190348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.51ns 
190349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
193181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
194058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
194062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
194064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
194064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
194065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
196915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
197802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
197808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
197810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
197810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.71ns 
197811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
200570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
201435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
201549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105.24ms 
201551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
201552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.61ns 
201553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
204282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
205188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
205289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.27ms 
205292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
205292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.21ns 
205293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
208006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
208897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
208901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
208902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
208902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.91ns 
208903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
211643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
212532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
212572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.27ms 
212576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
212580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.14ms 
212581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
215374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
216265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
216294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.41ms 
216296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
216296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
216297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
218998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
219905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
219908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
219910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
219910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
219912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
222685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
223574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
223731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 145.26ms 
223734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
223734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.12ns 
223735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
226583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
227481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
227493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.94ms 
227495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
227495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.51ns 
227496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
230262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
231143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
231156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ms 
231158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
231158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
231159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
233920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
234816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
234843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.48ms 
234844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
234844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
234845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
237620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
238497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
238511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.57ms 
238514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
238514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
238515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
241246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
242122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
242126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
242129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
242129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.51ns 
242130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
244852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
245723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
245727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
245732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
245733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.51ns 
245734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
248502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
249366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
249387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ms 
249388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
249389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
249389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
252250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
253136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
253152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.25ms 
253153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
253154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
253155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
255916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
256859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
256881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.55ms 
256882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
256883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
256883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
259700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
260621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
260624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
260626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
260626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
260626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
263339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
264243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
264247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
264248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
264248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
264249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
266949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
267819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
267824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
267825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
267825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
267826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
270538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
271418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
271421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
271422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
271422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
271423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
274145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
275037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
275039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.32ns 
275041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
275041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
275042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
277781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
278651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
278655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
278656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
278656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
278658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
281392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
282243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
282246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
282248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
282248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
282249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
285014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
285904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
285947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40ms 
285950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
285951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.31ns 
285952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
288727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
289639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
289675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.37ms 
289677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
289677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.61ns 
289678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
292409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
293311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
293344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.53ms 
293345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
293345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
293346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
296088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
297004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
297053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.5ms 
297055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
297055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
297056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
299792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
300683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
300711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.9ms 
300712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
300712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
300713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
303470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
304338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
304399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.87ms 
304402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
304402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.11ns 
304403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
307098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
307970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
307999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.34ms 
308000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
308000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
308001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
310788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
311680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
311700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.95ms 
311702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
311702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
311703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
314426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
315315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
315342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.49ms 
315344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
315344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
315345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
318131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
319028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
319048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.25ms 
319049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
319049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
319050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
321790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
322700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
322727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.98ms 
322728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
322728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
322729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
325437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
326326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
326374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.34ms 
326378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
326378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.07ms 
326378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
329094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
330011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
330036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.21ms 
330037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
330037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
330038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
332842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
333714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
333735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.02ms 
333737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
333738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.71ms 
333739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
336497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
337350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
337370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.99ms 
337371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
337372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
337372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
340179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
341090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
341110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.66ms 
341112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
341112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
341113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
343824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
344727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
344748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.23ms 
344749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
344749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
344750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
347504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
348426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
348436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.37ms 
348438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
348438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.61ns 
348439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
351145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
352042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
352058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.45ms 
352060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
352060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
352061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
354800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
355690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
355694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
355696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
355697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.91ns 
355698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
358442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
359312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
359315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 732.33ns 
359316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
359317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.41ns 
359318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
362031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
362899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
362902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
362904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
362904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
362905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
365634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
366498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
366506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
366535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
366535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
366535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
369277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
370173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
370179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.51ms 
370181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
370181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
370182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
372938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
373855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
373869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.02ms 
373871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
373871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
373872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
376596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
377495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
377499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
377500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
377500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
377501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
380207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
381088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
381091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 685.03ns 
381092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
381092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
381093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
383815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
384705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
384711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
384712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
384712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
384713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
387444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
388299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
388302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.33ns 
388303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
388303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
388304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
391041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
391886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
391888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 612.43ns 
391890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
391890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
391890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
394656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
395538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
395540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 639.53ns 
395541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
395541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
395542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
398253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
399138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
399142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
399144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
399144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
399145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
401870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
402762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
402772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.44ms 
402774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
402774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
402775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
405556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
406448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
406452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
406454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
406454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
406455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
409187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
410084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
410091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
410092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
410092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
410093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
412824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
413697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
413702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
413704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
413704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
413704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
416478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
417359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
417381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.05ms 
417383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
417383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.11ns 
417384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
420136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
420996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
421000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
421002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
421002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
421002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
423740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
424643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
424646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
424647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
424648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
424648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
427374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
428279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
428284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
428285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
428285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
428286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
431024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
431926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
431944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.25ms 
431946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
431946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
431946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
434703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
435571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
435576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 410.72ns 
435578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
435578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
435579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
438305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
439209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
439249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.35ms 
439251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
439251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
439251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
442016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
442900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
442905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
442912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
442913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.91ns 
442914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
445651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
446523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
446541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.7ms 
446543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
446543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
446543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
449297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
450181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
450204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20ms 
450206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
450206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
450207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
452988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
453894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
453920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.51ms 
453921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
453922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
453922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
456715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
457628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
457630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 602.53ns 
457632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
457632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
457633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
460383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
461283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
461289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
461290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
461290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
461291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
464067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
464994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
464998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
464999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
464999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
465000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
467761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
468672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
468676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
468679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
468679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
468680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
471414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
472323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
472326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 997.54ns 
472327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
472327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
472328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
475091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
475997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
476001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
476004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
476004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
476005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
478759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
479658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
479661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
479663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
479663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
479663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
482400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
483327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
483337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.88ms 
483338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
483338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
483339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
486021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
486896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
486903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
486904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
486905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
486905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
489659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
490554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
490563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.87ms 
490565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
490565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.1ns 
490566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
493370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
494295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
494304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.13ms 
494306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
494306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
494307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
497065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
497978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
497983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
497984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
497984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
497985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
500730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
501636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
501641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
501643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
501643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
501643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
504411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
505300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
505302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 858.24ns 
505304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
505304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
505305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
508027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
508944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
508947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
508948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
508948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
508949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
511663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
512562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
512564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
512566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
512566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
512566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
515285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
516204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
516215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.47ms 
516216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
516216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
516217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
518960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
519864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
519868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
519870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
519871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.41ns 
519872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
522604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
523517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
523524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
523526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
523526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.01ns 
523527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
526279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
527207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
527209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 925.14ns 
527211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
527211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.31ns 
527212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
529966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
530888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
530890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 725.23ns 
530892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
530892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
530892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
533639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
534566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
534570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
534572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
534572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
534573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
537351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
538287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
538290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 957.14ns 
538291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
538292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
538293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
541076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
541988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
541991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
541993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
541993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
541993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
544720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
545627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
545629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
545631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
545631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
545631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
548406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
549345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
549350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
549356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
549356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.51ns 
549357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
552163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
553061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
553064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 973.54ns 
553066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
553066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
553066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
555777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
556713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
556727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.51ms 
556728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
556728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
556729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
559533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
560468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
560471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
560472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
560472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
560473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
563242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
564185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
564192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
564193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
564193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
564194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
566955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
567845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
567848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
567850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
567850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.71ns 
567851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
570645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
571562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
571565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 969.24ns 
571566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
571567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
571567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
574321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
575241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
575245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
575246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
575247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
575247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
577992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
578917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
578920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
578921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
578922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
578923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
581728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
582647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
582652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
582653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
582653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
582654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
585457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
586356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
586360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
586361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
586361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
586362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
589122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
590037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
590042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
590044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
590044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
590045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
592787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
593714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
593723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.18ms 
593725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
593725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
593726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
596517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
597430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
597441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.76ms 
597442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
597443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
597443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
600224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
601147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
601154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
601156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
601156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
601157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
603905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
604830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
604838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
604839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
604840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
604840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
607595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
608535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
608548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.45ms 
608550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
608550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
608551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
611322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
612271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
612287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.58ms 
612288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
612288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
612289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
615130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
616068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
616080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.69ms 
616081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
616081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
616082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
618890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
619802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
619810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.66ms 
619812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
619812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
619813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
622590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
623506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
623533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.69ms 
623535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
623535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
623536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
626373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
627300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
627329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.92ms 
627330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
627330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
627331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
630066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
631005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
631031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.9ms 
631033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
631033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
631034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
633777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
634738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
634770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.67ms 
634771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
634771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
634772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
637533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
638441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
638465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.95ms 
638467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
638467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
638468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
641228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
642141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
642206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.6ms 
642207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
642207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
642208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
644990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
645947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
645952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
645954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
645954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
645955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
648754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
649662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
649668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
649669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
649669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
649670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
652486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
653463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
653467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
653468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
653468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
653469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
656281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
657202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
657221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.69ms 
657222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
657222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
657223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
660061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
660975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
660983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.73ms 
660984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
660985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
660985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
663749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
664656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
664660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
664661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
664661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
664662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
667452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
668383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
668395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.89ms 
668397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
668398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
668398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
671222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
672145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
672159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.23ms 
672160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
672160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
672161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
674972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
675870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
675887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.97ms 
675888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
675888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
675889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
678730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
679619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
679622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
679624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
679624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
679624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
682445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
683378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
683382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
683383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
683383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
683384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
686219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
687135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
687141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
687143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
687143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
687143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
689897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
690832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
690838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
690839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
690839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
690840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
693589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
694507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
694564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52ms 
694567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
694567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
694568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
697354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
698250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
698278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.39ms 
698280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
698280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.71ns 
698281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
701087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
702036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
702050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
702052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
702052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
702052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
704821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
705751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
705754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 263.81ns 
705755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
705755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
705756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
708574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
709476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
709592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105.49ms 
709594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
709594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.51ns 
709595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
712354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
713271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
713317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.12ms 
713319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
713319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
713320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
716078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
716993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
716995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 268.21ns 
716997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
716997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
716998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
719793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
720737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
720739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 259.21ns 
720741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
720741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
720741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
723462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
724385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
724387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.11ns 
724389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
724389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
724389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
727133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
728051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
728053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 402.42ns 
728054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
728054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
728055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
730841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
731777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
731887     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
731899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 118.54ms 
731901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
731901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.81ns 
731904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
734757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
735723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
735774     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
735775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.76ms 
735777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
735777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.51ns 
735778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
738646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
739574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
739575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ns 
739613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
739659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
739684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
739694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
739713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
739714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
739716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
739717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
739723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
739723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
739728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
739730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
740017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
740018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
740020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
740021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
740022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
740184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
740185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
740188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
740190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
740191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
740192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
740407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
740409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
740411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
740411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
740413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
740417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
740569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
740571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
740573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
740573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
740574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
740575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
740585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
740586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
740587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
740590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
740592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
740593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
740603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
740605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
740606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
740607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
740607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
740608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
740766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
740767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
740769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
740919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
740920     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)'' 
740921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
740924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
740925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
740926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
740926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
740929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
740933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
740934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
740936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
740937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
740938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
741068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
741072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
741073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
741074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
741075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
741076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
741077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
741246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
741248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
741249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
741252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
741253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
741253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
741255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
741256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
741387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
741389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
741507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
741512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
741519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
741520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
741522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
741524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
741524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
741525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
741525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
741526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
741538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
741544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
741696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
741697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
741700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
741701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
741702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
741702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
741703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
741703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
741792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
741801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
741956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
741957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
741960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
741961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
741963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
741964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
742148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
742153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
742156     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)'' 
742158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
742160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
742160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
742161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
742162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
742175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
742180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
742182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
742183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
742336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
742337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
742339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
742340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
742341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
742342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
742589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
742590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
742591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
742593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
742594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
742595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
742596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
742597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
742796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
742797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
742959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
742960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
742961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
742968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
742974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
742982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
743172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
743174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
743175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
743176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
743190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
743322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
748125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
748127     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)'' 
748134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
748137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
748138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
748138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
748140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
748151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
748152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
748153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
748154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
748155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
748287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
748291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
748292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
748293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
748293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
748294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
748295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
748427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
748428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
748429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
748432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
748433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
748433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
748434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
748434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
748535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
748537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
748646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
748651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
748656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
748657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
748658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
748659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
748672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
748780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
748781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
748782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
748783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
748876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
748889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
748890     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)'' 
748891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
748893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
748893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
748894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
748895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
748907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
748908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
748909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
748911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
748912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
749022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
749023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
749025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
749027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
749028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
749191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
749196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
749196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
749197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
749198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
749199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
749199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
749323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
749324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
749325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
749326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
749327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
749328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
749328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
749329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
749329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
749330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
749331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
749332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
749332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
749333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
749333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
749439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
749440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
749447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
749536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
749631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
749632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
749633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
749634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
749635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
749635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
749636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
749636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
749636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
749739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
749746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
749848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
749849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
749850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
749851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
749851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
749852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
749852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
749853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
749858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
749860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
749982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
749991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
749999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
750126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
750127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
750128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
750129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
750130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
750130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
750130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
750131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
750199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
750200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
750200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
750201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
750202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
750208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
750214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
750350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
750452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
750453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
750453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
750454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
750645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
750747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
750748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
754216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
754221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
754222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
754223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
754224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
754354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
754355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
754356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
754357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
754358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
754481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
757852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
761370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
761375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
761376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
761377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
761378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
761570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
761571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
761572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
761573     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)' ...' 
761574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
762884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
762884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.91ns 
762885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
765789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
766830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
766831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
766832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
766839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
766849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
766852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
766854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
766855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
766860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
766861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
766864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
766865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
766867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
766877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
766878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
766880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
766930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
766931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
766932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
766932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
766933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
767007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
767008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
767008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
767009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
767010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
767014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
767014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
767015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
767015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
767016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
767017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
767111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
767112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
767113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
767113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
767115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
767115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
767216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
767217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
767218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
767218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
767219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
767220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
767220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
767221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
767222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
767222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
767223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
767223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
767224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
767225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
767226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
767226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
767227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
767228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
767228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
767232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
767273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
767274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
767346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
767348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
767349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
767350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
767351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
767352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
767401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
767404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
767406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
767406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
767408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
767409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
767410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
767458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
767461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
767466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
767525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
767587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
767587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.61ns 
767588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
770521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
771547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
771569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.98ms