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

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

Test	Method name	Duration	Result
powPositive	data()[100]	3.584s	passed
powPositiveConcrete	data()[101]	3.564s	passed
powGeq1Concrete	data()[102]	3.575s	passed
pow2InIntLower	data()[103]	3.635s	passed
pow2InIntUpper	data()[104]	3.578s	passed
logSelfConcrete	data()[105]	3.630s	passed
log1Concrete	data()[106]	3.640s	passed
logProduct	data()[107]	3.628s	passed
logTimesBaseConcrete	data()[108]	3.607s	passed
logProdIdentity	data()[109]	3.622s	passed
moduloByteIsInByte	data()[10]	3.798s	passed
logProdIdentityConcrete	data()[110]	3.593s	passed
logPowIdentity	data()[111]	3.632s	passed
logPowIdentityConcrete	data()[112]	3.631s	passed
logPositive	data()[113]	3.618s	passed
logPositiveConcrete	data()[114]	3.629s	passed
logMono	data()[115]	3.736s	passed
logMonoConcrete	data()[116]	3.593s	passed
powLogLess	data()[117]	3.655s	passed
powLogMore2	data()[118]	3.628s	passed
logLessThanPow	data()[119]	3.664s	passed
moduloCharIsInChar	data()[11]	3.754s	passed
logLessThanPowConcrete	data()[120]	3.629s	passed
logSqueeze	data()[121]	3.641s	passed
ifthenelse_equals	data()[122]	3.652s	passed
ifthenelse_equals_1	data()[123]	3.614s	passed
ifthenelse_equals_2	data()[124]	3.619s	passed
disjointWithSingleton1	data()[125]	3.583s	passed
disjointWithSingleton2	data()[126]	3.620s	passed
disjointArrayRanges	data()[127]	3.622s	passed
disjointArrayRangeAllFields1	data()[128]	3.612s	passed
disjointArrayRangeAllFields2	data()[129]	3.559s	passed
div_unique1	data()[12]	3.835s	passed
seqSelfDefinition	data()[130]	3.607s	passed
seqOutsideValue	data()[131]	3.635s	passed
castedGetAny	data()[132]	3.599s	passed
seqGetAlphaCast	data()[133]	3.604s	passed
getOfSeqSingleton	data()[134]	3.576s	passed
getOfSeqSingletonConcrete	data()[135]	3.553s	passed
getOfSeqConcat	data()[136]	3.573s	passed
getOfSeqSub	data()[137]	3.630s	passed
getOfSeqReverse	data()[138]	3.634s	passed
lenOfSeqEmpty	data()[139]	3.712s	passed
div_unique2	data()[13]	3.842s	passed
lenOfSeqSingleton	data()[140]	3.664s	passed
lenOfSeqConcat	data()[141]	3.624s	passed
lenOfSeqSub	data()[142]	3.657s	passed
lenOfSeqReverse	data()[143]	3.633s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.873s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.768s	passed
getOfSeqSingletonEQ	data()[146]	3.656s	passed
getOfSeqConcatEQ	data()[147]	3.670s	passed
getOfSeqSubEQ	data()[148]	3.694s	passed
getOfSeqReverseEQ	data()[149]	3.641s	passed
div_exists	data()[14]	3.897s	passed
lenOfSeqEmptyEQ	data()[150]	3.710s	passed
lenOfSeqSingletonEQ	data()[151]	3.784s	passed
lenOfSeqConcatEQ	data()[152]	3.779s	passed
lenOfSeqSubEQ	data()[153]	3.773s	passed
lenOfSeqReverseEQ	data()[154]	3.663s	passed
getOfSeqDefEQ	data()[155]	3.672s	passed
lenOfSeqDefEQ	data()[156]	3.650s	passed
seqConcatWithSeqEmpty1	data()[157]	3.664s	passed
seqConcatWithSeqEmpty2	data()[158]	3.716s	passed
seqReverseOfSeqEmpty	data()[159]	3.703s	passed
div_one	data()[15]	3.797s	passed
subSeqComplete	data()[160]	3.667s	passed
subSeqTailR	data()[161]	3.638s	passed
subSeqTailL	data()[162]	3.682s	passed
subSeqTailEQR	data()[163]	3.742s	passed
subSeqTailEQL	data()[164]	3.655s	passed
seqDef_split	data()[165]	3.718s	passed
seqDef_induction_upper	data()[166]	3.684s	passed
seqDef_induction_upper_concrete	data()[167]	3.632s	passed
seqDef_induction_lower	data()[168]	3.648s	passed
seqDef_induction_lower_concrete	data()[169]	3.653s	passed
jdiv_one	data()[16]	3.775s	passed
seqDef_split_in_three	data()[170]	3.695s	passed
seqDef_empty	data()[171]	3.686s	passed
seqDef_one_summand	data()[172]	3.636s	passed
seqDef_lower_equals_upper	data()[173]	3.593s	passed
seqDefOfSeq	data()[174]	3.610s	passed
seqSelfDefinitionEQ2	data()[175]	3.590s	passed
indexOfSeqSingleton	data()[176]	3.615s	passed
indexOfSeqConcatFirst	data()[177]	3.583s	passed
indexOfSeqConcatSecond	data()[178]	3.599s	passed
indexOfSeqSub	data()[179]	3.606s	passed
div_zero	data()[17]	3.762s	passed
lenOfArray2seq	data()[180]	3.599s	passed
getAnyOfArray2seq	data()[181]	3.604s	passed
getOfArray2seq	data()[182]	3.577s	passed
getAnyOfNPermInv	data()[183]	3.587s	passed
seqNPermRange	data()[184]	3.591s	passed
seqPermTrans	data()[185]	3.532s	passed
seqPermRefl	data()[186]	3.579s	passed
seqPermSplit	data()[187]	3.639s	passed
seqNPermRight	data()[188]	3.701s	passed
seqPermFromSwap	data()[189]	3.606s	passed
divResZero1	data()[18]	3.701s	passed
seqPermTransAlt0	data()[190]	3.592s	passed
seqPermTransAlt1	data()[191]	3.615s	passed
seqPermTransAlt2	data()[192]	3.619s	passed
seqPermTransAlt3	data()[193]	3.623s	passed
seqPermForall	data()[194]	3.777s	passed
seqPermExists	data()[195]	3.782s	passed
schiffl_lemma_2	data()[196]	25.430s	passed
schiffl_thm_1	data()[197]	4.495s	passed
eqSameSeq	data()[198]	3.748s	passed
divResZero2	data()[19]	3.689s	passed
eqTermCut	data()[1]	4.644s	passed
divResOne1	data()[20]	3.714s	passed
divResOne2	data()[21]	3.781s	passed
div_cancel1	data()[22]	3.643s	passed
div_cancel2	data()[23]	3.648s	passed
divAddMultDenom	data()[24]	3.648s	passed
divMinus	data()[25]	3.637s	passed
divMinusDenom	data()[26]	3.671s	passed
divLeastDPos	data()[27]	3.616s	passed
divLeastDNeg	data()[28]	3.667s	passed
divGreatestDPos	data()[29]	3.602s	passed
equivAllRight	data()[2]	4.092s	passed
divGreatestDNeg	data()[30]	3.582s	passed
divIncreasingPos	data()[31]	3.560s	passed
divIncreasingNeg	data()[32]	3.546s	passed
jdiv_zero	data()[33]	3.511s	passed
jdivPulloutMinusNum	data()[34]	3.667s	passed
jdivPulloutMinusDenom	data()[35]	3.656s	passed
jdiv_uniquePosPos	data()[36]	3.685s	passed
jdiv_uniquePosNeg	data()[37]	3.659s	passed
jdiv_uniqueNegPos	data()[38]	3.639s	passed
jdiv_uniqueNegNeg	data()[39]	3.687s	passed
irrflConcrete1	data()[3]	3.983s	passed
jdivMultDenom1	data()[40]	3.774s	passed
jdivMultDenom2	data()[41]	3.650s	passed
mod_geZero	data()[42]	3.640s	passed
mod_lessDenom	data()[43]	3.653s	passed
jmod_NumPos	data()[44]	3.701s	passed
jmod_NumNeg	data()[45]	3.641s	passed
jmod_geZero	data()[46]	3.706s	passed
jmodNumZero	data()[47]	3.680s	passed
jmod_pulloutminusNum	data()[48]	3.698s	passed
jmod_pulloutminusDenom	data()[49]	3.622s	passed
irrflConcrete2	data()[4]	3.889s	passed
jmodUnique1	data()[50]	3.726s	passed
jmodUnique2	data()[51]	3.738s	passed
intDivRem	data()[52]	3.602s	passed
jmodjmod	data()[53]	3.742s	passed
jmodDivisible	data()[54]	3.677s	passed
jmodDivisibleRep	data()[55]	3.648s	passed
jdivAddMultDenom	data()[56]	3.838s	passed
jmodAltZero	data()[57]	3.709s	passed
jmodAddMultDenomZero	data()[58]	3.619s	passed
polyDiv_zero	data()[59]	3.610s	passed
cancel_gtPos	data()[5]	3.876s	passed
polyMod_ltdivDenom	data()[60]	3.666s	passed
bsum_empty	data()[61]	3.694s	passed
bsum_induction_upper	data()[62]	3.758s	passed
bsum_induction_lower	data()[63]	3.644s	passed
bsum_num_of_bounds	data()[64]	3.649s	passed
bsum_num_of_bounds2	data()[65]	3.621s	passed
bsum_induction_upper2	data()[66]	3.701s	passed
bsum_induction_upper_concrete	data()[67]	3.630s	passed
bsum_induction_upper_concrete_2	data()[68]	3.645s	passed
bsum_induction_upper2_concrete	data()[69]	3.672s	passed
cancel_gtNeg	data()[6]	3.736s	passed
bsum_induction_lower_concrete	data()[70]	3.801s	passed
bsum_induction_lower2	data()[71]	3.635s	passed
bsum_induction_lower2_concrete	data()[72]	3.627s	passed
bsum_positive	data()[73]	3.693s	passed
bsum_upper_bound	data()[74]	3.665s	passed
bsum_lower_bound	data()[75]	3.648s	passed
bsum_positive_lower_bound_element	data()[76]	3.669s	passed
bsum_sub_same_index	data()[77]	3.689s	passed
bsum_less_same_index	data()[78]	3.630s	passed
bsum_equal_except_one_index	data()[79]	3.640s	passed
moduloIntIsInInt	data()[7]	3.698s	passed
bsum_num_of_is_max	data()[80]	3.673s	passed
bsum_num_of_is_max2	data()[81]	3.673s	passed
bsum_num_of_is_max3	data()[82]	3.664s	passed
bsum_num_of_is_max4	data()[83]	3.666s	passed
bsum_num_of_lt_max	data()[84]	3.669s	passed
bsum_num_of_lt_max2	data()[85]	3.737s	passed
bsum_num_of_lt_max3	data()[86]	3.652s	passed
bsum_num_of_lt_max4	data()[87]	3.671s	passed
bsum_num_of_gt0	data()[88]	3.644s	passed
bsum_num_of_gt0_alt	data()[89]	3.676s	passed
moduloLongIsInLong	data()[8]	3.719s	passed
bsum_add_concrete	data()[90]	3.599s	passed
bprod_all_positive	data()[91]	3.557s	passed
bprod_split	data()[92]	3.520s	passed
powConcrete0	data()[93]	3.576s	passed
powConcrete1	data()[94]	3.615s	passed
powSplitFactor	data()[95]	3.554s	passed
powAdd	data()[96]	3.569s	passed
powMono	data()[97]	3.548s	passed
powMonoConcrete	data()[98]	3.578s	passed
powMonoConcreteRight	data()[99]	3.622s	passed
moduloShortIsInShort	data()[9]	3.714s	passed
Standard output

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

2160       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2163       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2168       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2168       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4025       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10092      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.12s 
10196      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10239      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.7ns 
10255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.51ns 
10262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13787      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
13790      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14861      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14889      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.73ms 
14904      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14905      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 906.33ns 
14907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17962      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
17963      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
18993      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
18996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
18997      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.61ns 
18999      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
21927      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
22962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
22974      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.38ms 
22981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
22981      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.01ns 
22984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25902      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
25903      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
26862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
26867      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
26871      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
26871      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.81ns 
26872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29717      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
29718      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
30679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
30743      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.44ms 
30749      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
30749      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 474.41ns 
30750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33548      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
33548      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
34463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
34481      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.86ms 
34485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
34486      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.91ns 
34487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37275      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
37276      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
38177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
38181      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 806.52ns 
38184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
38184      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.61ns 
38185      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41012      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
41013      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
41896      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
41899      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.02ns 
41903      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
41904      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.81ns 
41905      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44645      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
44646      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
45606      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
45611      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
45617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
45617      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.71ns 
45619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48454      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
48455      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
49407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
49413      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
49416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
49417      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.2ns 
49420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52181      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
52182      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
53164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
53167      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 729.52ns 
53171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
53172      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 446.41ns 
53173      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56008      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
56009      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
56965      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
57004      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.38ms 
57006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
57006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.8ns 
57007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59872      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
59873      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
60775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
60844      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.3ms 
60849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
60849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.91ns 
60852      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63621      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
63622      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
64519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
64742      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 213.06ms 
64746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
64747      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.5ns 
64748      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
67601      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
68537      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
68542      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
68544      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
68544      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.2ns 
68545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71357      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
71358      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
72309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
72316      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
72319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
72319      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.01ns 
72320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75123      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
75124      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
76038      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
76080      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.42ms 
76082      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
76083      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.21ns 
76084      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78853      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
78854      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
79767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
79781      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.88ms 
79784      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
79785      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.51ns 
79786      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82527      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
82528      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
83454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
83469      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.85ms 
83472      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
83475      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.15ms 
83479      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86249      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
86249      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
87169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
87184      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.06ms 
87186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
87186      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.71ns 
87188      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90072      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
90072      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
90952      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
90965      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.52ms 
90967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
90967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.4ns 
90968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93677      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
93677      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
94588      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
94608      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.77ms 
94610      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
94610      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.1ns 
94611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97325      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
97325      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
98253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
98256      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
98258      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
98258      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
98259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
100973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
101869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
101904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.48ms 
101906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
101907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.31ns 
101908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
104600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
105490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
105541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.29ms 
105544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
105544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.21ns 
105546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
108262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
109168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
109212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.3ms 
109218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
109220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.21ms 
109223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
111968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
112824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
112831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
112832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
112832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111ns 
112833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
115555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
116484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
116497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.88ms 
116499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
116499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.5ns 
116500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
119200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
120089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
120099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.79ms 
120101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
120101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.6ns 
120102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
122793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
123674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
123682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
123683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
123683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
123684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
126324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
127233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
127241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms 
127244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
127244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.4ns 
127245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
129898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
130781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
130787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
130789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
130789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
130790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
133447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
134294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
134298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
134299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
134299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
134300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
137081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
137955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
137965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms 
137966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
137966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
137967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
140653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
141583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
141621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.14ms 
141624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
141625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.91ns 
141626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
144358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
145288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
145307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
145309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
145309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.5ns 
145310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
148033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
148950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
148966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms 
148968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
148968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.6ns 
148969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
151682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
152588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
152605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.24ms 
152606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
152606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.3ns 
152607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
155397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
156277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
156293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.99ms 
156294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
156294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns 
156295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
159147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
160027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
160066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.42ms 
160068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
160068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.91ns 
160069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
162816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
163713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
163716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 960.32ns 
163718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
163718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
163719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
166435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
167352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
167357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
167358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
167358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.8ns 
167359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
170090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
171001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
171009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
171011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
171011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
171012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
173795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
174703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
174712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
174713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
174713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.6ns 
174714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
177455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
178335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
178352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
178354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
178354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns 
178355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
181155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
182050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
182058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
182059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
182059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
182060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
184859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
185735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
185738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
185740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
185741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.11ns 
185742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
188512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
189432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
189436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
189438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
189438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
189438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
192148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
193054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
193058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
193059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
193060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
193061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
195794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
196720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
196784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.07ms 
196786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
196786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.2ns 
196787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
199533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
200445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
200522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.72ms 
200525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
200525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.7ns 
200526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
203247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
204122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
204125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
204126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
204126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.4ns 
204127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
206957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
207833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
207867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.43ms 
207869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
207869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123ns 
207870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
210605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
211520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
211545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.16ms 
211546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
211546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
211547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
214278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
215189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
215192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
215194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
215194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
215195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
217936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
218883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
219024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127.23ms 
219032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
219033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.71ns 
219034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
221817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
222729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
222739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ms 
222740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
222740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.4ns 
222741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
225457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
226351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
226358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
226359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
226359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.3ns 
226360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
229078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
229952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
229968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.98ms 
229970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
229970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
229971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
232733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
233618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
233631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.97ms 
233637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
233637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.41ns 
233638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
236415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
237323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
237328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
237330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
237330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
237331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
240175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
241083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
241087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
241090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
241091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.38ms 
241092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
243813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
244715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
244731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.71ms 
244732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
244732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
244733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
247457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
248367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
248380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ms 
248382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
248382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
248383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
251111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
251989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
252001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.99ms 
252003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
252003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.81ns 
252004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
254819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
255699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
255702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
255703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
255704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
255704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
258425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
259329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
259333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
259334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
259334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.81ns 
259335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
262063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
262972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
262977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
262978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
262978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
262979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
265710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
266645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
266649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
266651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
266651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.11ns 
266653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
269541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
270448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
270450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 568.43ns 
270452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
270452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
270453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
273205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
274082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
274085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
274087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
274087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.41ns 
274088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
276830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
277710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
277712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 885.84ns 
277714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
277714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
277715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
280447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
281368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
281405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.7ms 
281408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
281408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.71ns 
281409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
284139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
285042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
285070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.65ms 
285072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
285072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.81ns 
285073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
287795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
288696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
288718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.9ms 
288720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
288720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.42ns 
288721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
291453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
292357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
292387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.95ms 
292389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
292389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.91ns 
292389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
295140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
296057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
296076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.35ms 
296077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
296077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.61ns 
296078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
298796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
299668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
299706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.35ms 
299708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
299708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.61ns 
299709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
302450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
303325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
303346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18ms 
303348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
303348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.42ns 
303349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
306100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
307004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
307019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.57ms 
307020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
307021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.01ns 
307021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
309738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
310675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
310692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.25ms 
310694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
310694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.72ns 
310695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
313432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
314341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
314356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.87ms 
314358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
314358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.32ns 
314359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
317098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
318003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
318022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.34ms 
318023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
318023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.81ns 
318024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
320767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
321666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
321691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.99ms 
321692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
321692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.32ns 
321693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
324531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
325410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
325428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.38ms 
325430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
325430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.61ns 
325431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
328184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
329063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
329080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.99ms 
329081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
329082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.51ns 
329082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
331828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
332733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
332751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.99ms 
332753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
332753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.11ns 
332754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
335467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
336378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
336395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms 
336397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
336397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.51ns 
336398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
339125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
340054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
340071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.36ms 
340073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
340073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.51ns 
340074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
342770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
343663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
343670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
343672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
343673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.91ns 
343674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
346348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
347214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
347227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.45ms 
347229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
347229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.62ns 
347230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
349889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
350744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
350747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
350749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
350749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.91ns 
350750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
353421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
354321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
354323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.25ns 
354325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
354325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.61ns 
354325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
357033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
357936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
357938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.17ns 
357940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
357940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.91ns 
357940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
360602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
361486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
361492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
361494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
361494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.91ns 
361494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
364169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
365055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
365061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
365064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
365064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.12ns 
365065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
367745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
368598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
368609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
368610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
368610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.51ns 
368611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
371314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
372184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
372187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
372188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
372188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.61ns 
372189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
374910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
375807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
375810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.52ns 
375811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
375811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
375812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
378499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
379388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
379394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
379395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
379395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.51ns 
379396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
382062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
382955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
382958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 550.34ns 
382959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
382959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.81ns 
382960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
385640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
386530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
386532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 554.54ns 
386534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
386534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.81ns 
386534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
389254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
390165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
390167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 654.25ns 
390169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
390169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.01ns 
390169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
392868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
393742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
393746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
393747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
393747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
393748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
396497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
397368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
397375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.45ms 
397377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
397377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.41ns 
397378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
400109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
401012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
401015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
401016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
401017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.31ns 
401017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
403734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
404637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
404643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
404644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
404645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.71ns 
404645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
407351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
408246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
408251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
408252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
408252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.91ns 
408253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
410963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
411859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
411872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.55ms 
411874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
411874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.51ns 
411874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
414582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
415462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
415466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
415467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
415467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.41ns 
415468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
418218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
419094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
419097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
419099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
419099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.01ns 
419100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
421810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
422724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
422728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
422729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
422729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.71ns 
422730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
425434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
426332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
426346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ms 
426347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
426348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.21ns 
426348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
429055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
429969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
429974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 353.44ns 
429977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
429977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.12ns 
429978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
432789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
433682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
433711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.8ms 
433713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
433713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.71ns 
433714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
436424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
437300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
437304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
437305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
437305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.51ns 
437306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
440056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
440939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
440959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.86ms 
440962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
440962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.93ns 
440964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
443673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
444572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
444588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms 
444589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
444589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.91ns 
444590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
447306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
448231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
448252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.85ms 
448253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
448253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.21ns 
448254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
450972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
451878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
451880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 537.45ns 
451883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
451883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.82ns 
451884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
454614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
455516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
455522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
455523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
455523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
455524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
458260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
459170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
459173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
459175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
459175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.81ns 
459176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
461904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
462784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
462787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 858.05ns 
462788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
462789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
462789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
465539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
466404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
466406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 782.17ns 
466408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
466408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.31ns 
466409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
469077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
469986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
469990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
469991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
469991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.01ns 
469992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
472694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
473606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
473609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
473611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
473611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.41ns 
473613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
476317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
477222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
477231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.15ms 
477232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
477232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.11ns 
477233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
479946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
480837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
480844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
480845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
480845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.11ns 
480846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
483520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
484395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
484402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
484404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
484404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
484404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
487123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
487997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
488009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ms 
488011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
488012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.92ns 
488013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
490732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
491640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
491644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
491646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
491646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.42ns 
491647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
494333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
495239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
495244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
495247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
495248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
495248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
497933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
498847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
498850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 753.66ns 
498851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
498851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.21ns 
498852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
501528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
502422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
502425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.28ns 
502426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
502426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.51ns 
502427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
505096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
505975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
505978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
505979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
505980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.31ns 
505980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
508667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
509542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
509551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
509553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
509553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.51ns 
509553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
512292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
513178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
513181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
513182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
513182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
513183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
515895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
516809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
516815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
516817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
516817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.71ns 
516817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
519573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
520524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
520527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
520528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
520528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
520529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
523270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
524190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
524192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.55ns 
524193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
524193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
524194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
526901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
527812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
527815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
527816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
527816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
527817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
530554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
531470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
531473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 876.46ns 
531474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
531474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
531475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
534210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
535102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
535105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
535107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
535107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
535107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
538027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
538974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
538978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
538980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
538980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.11ns 
538981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
541855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
542742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
542746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
542748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
542748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
542749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
545464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
546399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
546402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 868.75ns 
546403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
546404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
546404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
549144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
550063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
550072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
550074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
550074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
550074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
552823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
553764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
553766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.13ns 
553767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
553767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
553768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
556486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
557401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
557407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
557409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
557409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.91ns 
557410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
560150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
561114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
561117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 930.05ns 
561118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
561118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
561119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
563946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
564899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
564901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 906.56ns 
564903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
564903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
564904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
567733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
568677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
568681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
568682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
568682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
568683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
571515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
572450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
572453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
572455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
572455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
572456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
575202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
576114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
576117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
576118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
576118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
576119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
578845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
579785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
579788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
579791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
579791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
579792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
582521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
583436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
583440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
583442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
583442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
583443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
586180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
587096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
587105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
587106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
587106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
587107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
589850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
590811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
590820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.83ms 
590821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
590821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.81ns 
590822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
593592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
594517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
594524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
594525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
594525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
594526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
597269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
598183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
598190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
598192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
598192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
598193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
600904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
601817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
601828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
601830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
601830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
601831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
604584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
605499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
605511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ms 
605512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
605512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.51ns 
605513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
608289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
609241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
609252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.52ms 
609254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
609254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
609255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
611985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
612898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
612907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.99ms 
612909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
612910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.81ns 
612911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
615677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
616602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
616625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.88ms 
616626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
616626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
616627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
619354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
620284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
620309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.44ms 
620311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
620311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
620312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
623015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
623919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
623941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.09ms 
623942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
623942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
623943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
626663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
627568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
627589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.18ms 
627590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
627590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
627591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
630307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
631220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
631242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.67ms 
631243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
631243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
631244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
634002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
634883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
634937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.45ms 
634939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
634939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
634940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
637702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
638618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
638624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
638625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
638625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
638626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
641348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
642254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
642259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
642260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
642260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
642261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
644946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
645849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
645852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
645854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
645854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
645855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
648520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
649447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
649462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.31ms 
649463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
649463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
649464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
652136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
653045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
653052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
653053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
653053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
653054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
655777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
656664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
656667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
656669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
656669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
656669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
659371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
660239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
660250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.52ms 
660251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
660252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
660252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
662945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
663837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
663849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
663850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
663851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
663851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
666526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
667438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
667455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms 
667457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
667457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.91ns 
667458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
670149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
671051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
671054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
671055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
671055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
671056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
673740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
674654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
674658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
674659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
674659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
674660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
677354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
678229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
678235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 
678237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
678237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
678237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
680931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
681817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
681822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
681826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
681826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.28ns 
681827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
684471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
685369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
685415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.79ms 
685416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
685417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
685417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
688033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
688928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
688947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.11ms 
688949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
688949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
688950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
691647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
692514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
692527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.82ms 
692528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
692528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
692529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
695249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
696163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
696165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 170.47ns 
696167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
696167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.12ns 
696168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
698873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
699772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
699866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.57ms 
699869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
699869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.53ns 
699870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
702533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
703437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
703473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.93ms 
703475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
703475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.71ns 
703476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
706181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
707063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
707065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 197.12ns 
707066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
707066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.11ns 
707067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
709766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
710678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
710680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 233.02ns 
710681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
710682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.11ns 
710682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
713378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
714297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
714299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.61ns 
714300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
714300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
714301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
717033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
717921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
717923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 382.94ns 
717924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
717924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.81ns 
717925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
720658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
721573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
721690     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
721699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 123.81ms 
721702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
721702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.52ns 
721704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
724513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
725432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
725482     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
725482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.04ms 
725484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
725484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.81ns 
725485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
728243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
729132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
729134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 
729167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
729221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
729237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
729243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
729262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
729265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
729267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
729269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
729276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
729280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
729283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
729287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
729553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
729554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
729558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
729558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
729560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
729718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
729719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
729723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
729724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
729726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
729729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
729917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
729918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
729920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
729921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
729921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
729923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
730059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
730061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
730062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
730063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
730064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
730065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
730073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
730074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
730076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
730077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
730077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
730079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
730087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
730088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
730089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
730090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
730091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
730092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
730292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
730293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
730294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
730463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
730464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
730466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
730468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
730469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
730470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
730471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
730472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
730476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
730477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
730478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
730479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
730480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
730605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
730608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
730610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
730611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
730612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
730613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
730614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
730742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
730743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
730745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
730746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
730747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
730748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
730749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
730750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
730855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
730856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
730954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
730958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
730963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
730964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
730966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
730967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
730980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
730980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
730981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
730982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
730991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
731000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
731107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
731108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
731109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
731111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
731112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
731112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
731113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
731114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
731167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
731173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
731272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
731273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
731275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
731276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
731277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
731279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
731413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
731417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
731418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
731419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
731421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
731422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
731423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
731423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
731433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
731434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
731435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
731437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
731536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
731537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
731538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
731539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
731540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
731540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
731651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
731652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
731654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
731655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
731656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
731657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
731657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
731658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
731748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
731749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
731833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
731834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
731835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
731840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
731845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
731850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
731982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
731983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
731984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
731985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
731997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
732098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
736157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
736159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
736163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
736166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
736167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
736168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
736169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
736179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
736180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
736181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
736182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
736183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
736293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
736297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
736298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
736300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
736301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
736301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
736302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
736468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
736469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
736470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
736471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
736472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
736473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
736474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
736474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
736565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
736566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
736662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
736668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
736673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
736674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
736675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
736676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
736688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
736793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
736794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
736795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
736796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
736884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
736896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
736897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
736898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
736899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
736900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
736901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
736901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
736914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
736915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
736917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
736918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
736918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
737023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
737024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
737025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
737026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
737027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
737134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
737140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
737141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
737142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
737142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
737143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
737144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
737259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
737260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
737262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
737263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
737264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
737265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
737265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
737266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
737267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
737268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
737269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
737270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
737271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
737271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
737272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
737372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
737373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
737381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
737474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
737566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
737567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
737568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
737569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
737570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
737571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
737572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
737572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
737573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
737671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
737679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
737784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
737786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
737787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
737788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
737789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
737789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
737790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
737791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
737797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
737798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
737891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
737898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
737905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
738022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
738023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
738024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
738025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
738026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
738026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
738027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
738028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
738092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
738094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
738095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
738096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
738097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
738103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
738109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
738246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
738349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
738350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
738351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
738352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
738552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
738656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
738657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
742179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
742184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
742185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
742186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
742187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
742324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
742324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
742325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
742326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
742329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
742450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
745777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
749531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
749535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
749536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
749537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
749538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
749668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
749668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
749669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
749670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
749671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
750914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
750914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.21ns 
750915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
753755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
754700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
754702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
754703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
754712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
754722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
754724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
754726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
754728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
754733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
754734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
754739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
754739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
754742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
754753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
754753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
754755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
754809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
754810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
754811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
754811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
754812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
754882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
754883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
754884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
754885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
754885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
754890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
754890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
754891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
754891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
754892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
754893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
754977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
754978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
754979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
754979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
754981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
754982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
755067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
755068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
755069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
755070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
755070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
755071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
755072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
755073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
755074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
755074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
755075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
755075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
755076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
755076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
755077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
755078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
755078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
755079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
755080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
755083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
755120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
755122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
755179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
755180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
755181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
755182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
755184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
755184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
755229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
755232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
755233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
755234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
755236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
755237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
755238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
755287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
755289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
755292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
755349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
755409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
755409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.81ns 
755409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
758189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
759137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
759155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.95ms