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

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
198
tests
failures
ignored
11m2.33s
duration
100%
successful
Tests
Standard output
Tests

Test	Method name	Duration	Result
powPositive	data()[100]	3.185s	passed
powPositiveConcrete	data()[101]	3.179s	passed
powGeq1Concrete	data()[102]	3.194s	passed
pow2InIntLower	data()[103]	3.208s	passed
pow2InIntUpper	data()[104]	3.211s	passed
logSelfConcrete	data()[105]	3.220s	passed
log1Concrete	data()[106]	3.203s	passed
logProduct	data()[107]	3.208s	passed
logTimesBaseConcrete	data()[108]	3.199s	passed
logProdIdentity	data()[109]	3.227s	passed
moduloByteIsInByte	data()[10]	3.298s	passed
logProdIdentityConcrete	data()[110]	3.226s	passed
logPowIdentity	data()[111]	3.223s	passed
logPowIdentityConcrete	data()[112]	3.221s	passed
logPositive	data()[113]	3.235s	passed
logPositiveConcrete	data()[114]	3.229s	passed
logMono	data()[115]	3.210s	passed
logMonoConcrete	data()[116]	3.177s	passed
powLogLess	data()[117]	3.229s	passed
powLogMore2	data()[118]	3.246s	passed
logLessThanPow	data()[119]	3.248s	passed
moduloCharIsInChar	data()[11]	3.254s	passed
logLessThanPowConcrete	data()[120]	3.216s	passed
logSqueeze	data()[121]	3.204s	passed
ifthenelse_equals	data()[122]	3.199s	passed
ifthenelse_equals_1	data()[123]	3.197s	passed
ifthenelse_equals_2	data()[124]	3.210s	passed
disjointWithSingleton1	data()[125]	3.208s	passed
disjointWithSingleton2	data()[126]	3.215s	passed
disjointArrayRanges	data()[127]	3.221s	passed
disjointArrayRangeAllFields1	data()[128]	3.226s	passed
disjointArrayRangeAllFields2	data()[129]	3.229s	passed
div_unique1	data()[12]	3.275s	passed
seqSelfDefinition	data()[130]	3.221s	passed
seqOutsideValue	data()[131]	3.211s	passed
castedGetAny	data()[132]	3.200s	passed
seqGetAlphaCast	data()[133]	3.182s	passed
getOfSeqSingleton	data()[134]	3.183s	passed
getOfSeqSingletonConcrete	data()[135]	3.196s	passed
getOfSeqConcat	data()[136]	3.249s	passed
getOfSeqSub	data()[137]	3.257s	passed
getOfSeqReverse	data()[138]	3.200s	passed
lenOfSeqEmpty	data()[139]	3.184s	passed
div_unique2	data()[13]	3.301s	passed
lenOfSeqSingleton	data()[140]	3.219s	passed
lenOfSeqConcat	data()[141]	3.187s	passed
lenOfSeqSub	data()[142]	3.201s	passed
lenOfSeqReverse	data()[143]	3.198s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.187s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.186s	passed
getOfSeqSingletonEQ	data()[146]	3.213s	passed
getOfSeqConcatEQ	data()[147]	3.236s	passed
getOfSeqSubEQ	data()[148]	3.224s	passed
getOfSeqReverseEQ	data()[149]	3.219s	passed
div_exists	data()[14]	3.409s	passed
lenOfSeqEmptyEQ	data()[150]	3.210s	passed
lenOfSeqSingletonEQ	data()[151]	3.209s	passed
lenOfSeqConcatEQ	data()[152]	3.188s	passed
lenOfSeqSubEQ	data()[153]	3.209s	passed
lenOfSeqReverseEQ	data()[154]	3.211s	passed
getOfSeqDefEQ	data()[155]	3.191s	passed
lenOfSeqDefEQ	data()[156]	3.199s	passed
seqConcatWithSeqEmpty1	data()[157]	3.199s	passed
seqConcatWithSeqEmpty2	data()[158]	3.225s	passed
seqReverseOfSeqEmpty	data()[159]	3.207s	passed
div_one	data()[15]	3.243s	passed
subSeqComplete	data()[160]	3.214s	passed
subSeqTailR	data()[161]	3.228s	passed
subSeqTailL	data()[162]	3.245s	passed
subSeqTailEQR	data()[163]	3.223s	passed
subSeqTailEQL	data()[164]	3.216s	passed
seqDef_split	data()[165]	3.239s	passed
seqDef_induction_upper	data()[166]	3.249s	passed
seqDef_induction_upper_concrete	data()[167]	3.226s	passed
seqDef_induction_lower	data()[168]	3.263s	passed
seqDef_induction_lower_concrete	data()[169]	3.273s	passed
jdiv_one	data()[16]	3.242s	passed
seqDef_split_in_three	data()[170]	3.343s	passed
seqDef_empty	data()[171]	3.221s	passed
seqDef_one_summand	data()[172]	3.203s	passed
seqDef_lower_equals_upper	data()[173]	3.218s	passed
seqDefOfSeq	data()[174]	3.213s	passed
seqSelfDefinitionEQ2	data()[175]	3.216s	passed
indexOfSeqSingleton	data()[176]	3.191s	passed
indexOfSeqConcatFirst	data()[177]	3.232s	passed
indexOfSeqConcatSecond	data()[178]	3.219s	passed
indexOfSeqSub	data()[179]	3.218s	passed
div_zero	data()[17]	3.280s	passed
lenOfArray2seq	data()[180]	3.220s	passed
getAnyOfArray2seq	data()[181]	3.203s	passed
getOfArray2seq	data()[182]	3.208s	passed
getAnyOfNPermInv	data()[183]	3.206s	passed
seqNPermRange	data()[184]	3.303s	passed
seqPermTrans	data()[185]	3.232s	passed
seqPermRefl	data()[186]	3.226s	passed
seqPermSplit	data()[187]	3.207s	passed
seqNPermRight	data()[188]	3.384s	passed
seqPermFromSwap	data()[189]	3.275s	passed
divResZero1	data()[18]	3.261s	passed
seqPermTransAlt0	data()[190]	3.216s	passed
seqPermTransAlt1	data()[191]	3.220s	passed
seqPermTransAlt2	data()[192]	3.222s	passed
seqPermTransAlt3	data()[193]	3.191s	passed
seqPermForall	data()[194]	3.306s	passed
seqPermExists	data()[195]	3.295s	passed
schiffl_lemma_2	data()[196]	23.522s	passed
schiffl_thm_1	data()[197]	4.043s	passed
eqSameSeq	data()[198]	3.286s	passed
divResZero2	data()[19]	3.240s	passed
eqTermCut	data()[1]	3.737s	passed
divResOne1	data()[20]	3.245s	passed
divResOne2	data()[21]	3.261s	passed
div_cancel1	data()[22]	3.252s	passed
div_cancel2	data()[23]	3.223s	passed
divAddMultDenom	data()[24]	3.305s	passed
divMinus	data()[25]	3.286s	passed
divMinusDenom	data()[26]	3.291s	passed
divLeastDPos	data()[27]	3.234s	passed
divLeastDNeg	data()[28]	3.230s	passed
divGreatestDPos	data()[29]	3.231s	passed
equivAllRight	data()[2]	3.632s	passed
divGreatestDNeg	data()[30]	3.228s	passed
divIncreasingPos	data()[31]	3.224s	passed
divIncreasingNeg	data()[32]	3.230s	passed
jdiv_zero	data()[33]	3.263s	passed
jdivPulloutMinusNum	data()[34]	3.276s	passed
jdivPulloutMinusDenom	data()[35]	3.329s	passed
jdiv_uniquePosPos	data()[36]	3.279s	passed
jdiv_uniquePosNeg	data()[37]	3.254s	passed
jdiv_uniqueNegPos	data()[38]	3.221s	passed
jdiv_uniqueNegNeg	data()[39]	3.235s	passed
irrflConcrete1	data()[3]	3.548s	passed
jdivMultDenom1	data()[40]	3.262s	passed
jdivMultDenom2	data()[41]	3.226s	passed
mod_geZero	data()[42]	3.217s	passed
mod_lessDenom	data()[43]	3.214s	passed
jmod_NumPos	data()[44]	3.238s	passed
jmod_NumNeg	data()[45]	3.246s	passed
jmod_geZero	data()[46]	3.218s	passed
jmodNumZero	data()[47]	3.230s	passed
jmod_pulloutminusNum	data()[48]	3.224s	passed
jmod_pulloutminusDenom	data()[49]	3.201s	passed
irrflConcrete2	data()[4]	3.482s	passed
jmodUnique1	data()[50]	3.281s	passed
jmodUnique2	data()[51]	3.278s	passed
intDivRem	data()[52]	3.188s	passed
jmodjmod	data()[53]	3.226s	passed
jmodDivisible	data()[54]	3.249s	passed
jmodDivisibleRep	data()[55]	3.212s	passed
jdivAddMultDenom	data()[56]	3.355s	passed
jmodAltZero	data()[57]	3.213s	passed
jmodAddMultDenomZero	data()[58]	3.218s	passed
polyDiv_zero	data()[59]	3.209s	passed
cancel_gtPos	data()[5]	3.422s	passed
polyMod_ltdivDenom	data()[60]	3.210s	passed
bsum_empty	data()[61]	3.178s	passed
bsum_induction_upper	data()[62]	3.187s	passed
bsum_induction_lower	data()[63]	3.209s	passed
bsum_num_of_bounds	data()[64]	3.220s	passed
bsum_num_of_bounds2	data()[65]	3.258s	passed
bsum_induction_upper2	data()[66]	3.185s	passed
bsum_induction_upper_concrete	data()[67]	3.197s	passed
bsum_induction_upper_concrete_2	data()[68]	3.196s	passed
bsum_induction_upper2_concrete	data()[69]	3.197s	passed
cancel_gtNeg	data()[6]	3.307s	passed
bsum_induction_lower_concrete	data()[70]	3.197s	passed
bsum_induction_lower2	data()[71]	3.195s	passed
bsum_induction_lower2_concrete	data()[72]	3.198s	passed
bsum_positive	data()[73]	3.262s	passed
bsum_upper_bound	data()[74]	3.251s	passed
bsum_lower_bound	data()[75]	3.239s	passed
bsum_positive_lower_bound_element	data()[76]	3.245s	passed
bsum_sub_same_index	data()[77]	3.231s	passed
bsum_less_same_index	data()[78]	3.254s	passed
bsum_equal_except_one_index	data()[79]	3.228s	passed
moduloIntIsInInt	data()[7]	3.347s	passed
bsum_num_of_is_max	data()[80]	3.210s	passed
bsum_num_of_is_max2	data()[81]	3.221s	passed
bsum_num_of_is_max3	data()[82]	3.214s	passed
bsum_num_of_is_max4	data()[83]	3.233s	passed
bsum_num_of_lt_max	data()[84]	3.255s	passed
bsum_num_of_lt_max2	data()[85]	3.230s	passed
bsum_num_of_lt_max3	data()[86]	3.223s	passed
bsum_num_of_lt_max4	data()[87]	3.217s	passed
bsum_num_of_gt0	data()[88]	3.223s	passed
bsum_num_of_gt0_alt	data()[89]	3.209s	passed
moduloLongIsInLong	data()[8]	3.376s	passed
bsum_add_concrete	data()[90]	3.209s	passed
bprod_all_positive	data()[91]	3.215s	passed
bprod_split	data()[92]	3.196s	passed
powConcrete0	data()[93]	3.200s	passed
powConcrete1	data()[94]	3.199s	passed
powSplitFactor	data()[95]	3.222s	passed
powAdd	data()[96]	3.199s	passed
powMono	data()[97]	3.202s	passed
powMonoConcrete	data()[98]	3.182s	passed
powMonoConcreteRight	data()[99]	3.175s	passed
moduloShortIsInShort	data()[9]	3.284s	passed
Standard output

297        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
320        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.85ms 
528        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544        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)

1399       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1401       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1403       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1404       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2745       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8183       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.65s 
8270       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8306       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.4ns 
8320       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8321       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.73ms 
8326       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11056      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
11059      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12049      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.07ms 
12063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12064      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 458.71ns 
12066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
14840      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15677      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15691      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.77ms 
15693      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15693      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.6ns 
15694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
18372      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19218      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19235      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.76ms 
19242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19243      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.51ns 
19245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21876      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
21876      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22722      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 
22727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22728      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.03ms 
22730      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25313      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
25313      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26105      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26145      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.97ms 
26149      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26149      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.11ns 
26151      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28645      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
28645      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29453      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.41ms 
29457      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29457      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.11ns 
29459      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32003      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
32004      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32797      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32801      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.02ns 
32804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32805      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.81ns 
32806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35357      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
35358      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36178      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.91ns 
36181      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36181      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.41ns 
36182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
38676      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39461      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.31ns 
39464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39464      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.81ns 
39466      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41954      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
41955      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42760      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.61ns 
42763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42763      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.61ns 
42764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45231      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
45231      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46011      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46014      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 598.11ns 
46016      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46017      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.6ns 
46018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48477      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
48477      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49249      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49290      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.71ms 
49292      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49292      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.5ns 
49293      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51776      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
51776      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52554      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52591      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.28ms 
52595      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52596      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.41ns 
52597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55063      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
55063      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56000      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 155.49ms 
56004      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56004      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.41ns 
56006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58465      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
58465      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59244      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
59247      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59247      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.51ns 
59248      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61711      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
61712      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62483      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62486      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
62490      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62491      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.51ns 
62492      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64956      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
64957      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65730      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65767      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.74ms 
65770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65771      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.71ns 
65772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
68245      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69029      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.21ms 
69031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69031      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.9ns 
69032      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71472      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
71472      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
72269      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.88ms 
72271      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
72271      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.6ns 
72277      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74729      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
74730      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
75500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
75515      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.92ms 
75516      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
75516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.2ns 
75517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77986      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
77987      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
78776      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.54ms 
78777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
78777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.2ns 
78778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81208      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
81209      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82001      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82028      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.8ms 
82029      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.8ns 
82030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84446      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
84447      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
85247      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
85250      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
85251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
85251      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 
85252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87705      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
87707      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
88514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
88555      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.52ms 
88558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
88559      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.51ns 
88560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90985      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
90985      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
91777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
91842      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.5ms 
91844      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
91845      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.91ns 
91846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94291      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
94291      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
95085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95133      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.1ms 
95135      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95135      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.1ns 
95136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97567      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
97568      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
98360      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
98368      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.81ms 
98369      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
98369      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.1ns 
98370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
100786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
101583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
101597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.32ms 
101599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
101599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.9ns 
101600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
104027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
104817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
104829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
104830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
104830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.1ns 
104831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
107251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
108049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
108057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
108058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.4ns 
108059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
110483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
111273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
111281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
111282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
111282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
111283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
113705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
114503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
114511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.36ms 
114512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
114512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123ns 
114513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
116962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
117769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
117773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
117776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
117776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.71ns 
117777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
120233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
121024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
121048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.66ms 
121053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.81ns 
121055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
123521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
124327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
124379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.88ms 
124383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
124383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.81ns 
124395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
126855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
127643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
127660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.44ms 
127662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
127662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.3ns 
127663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
130096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
130896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
130913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 
130916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
130916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.21ns 
130917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
133327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
134112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
134135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.04ms 
134137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
134138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.31ns 
134139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
136557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
137350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
137370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms 
137372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
137372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.71ns 
137373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
139801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
140595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
140632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.28ms 
140635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
140635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.01ns 
140636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
143065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
143856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
143858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
143860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
143860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
143860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
146271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
147071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
147076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
147077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
147077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
147078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
149495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
150282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
150290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
150291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
150291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
150292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
152715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
153510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
153527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.83ms 
153530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
153531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.41ns 
153532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
155969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
156756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
156774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.89ms 
156776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
156776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
156776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
159190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
159984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
159992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.11ms 
159994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
159994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
159995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
162419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
163218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
163222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
163224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
163224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.01ns 
163225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
165657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
166442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
166446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
166448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
166448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
166449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
168858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
169643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
169647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
169648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
169649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
169650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
172066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
172856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
172928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.81ms 
172931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
172931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.51ns 
172932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
175338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
176125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
176206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.9ms 
176209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
176209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.71ns 
176210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
178606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
179390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
179394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
179396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
179397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.51ns 
179398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
181801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
182584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
182620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.86ms 
182622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
182623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 437.01ns 
182624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
185030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
185814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
185869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.11ms 
185872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
185872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.91ns 
185873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
188292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
189078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
189081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
189082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
189082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
189084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
191487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
192284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
192436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 140.46ms 
192439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
192439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.31ns 
192440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
194849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
195637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
195649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.27ms 
195651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
195651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163ns 
195652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
198073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
198859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
198867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.34ms 
198869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
198869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
198870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
201275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
202059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
202076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.07ms 
202077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
202077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
202078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
204492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
205273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
205286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.97ms 
205288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
205288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
205289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
207683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
208461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
208464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
208466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
208466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
208466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
210864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
211647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
211652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
211653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
211653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
211654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
214051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
214837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
214860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.2ms 
214862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
214862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
214863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
217268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
218063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
218080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.64ms 
218082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
218082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
218083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
220532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
221322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
221338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.43ms 
221339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
221339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
221340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
223734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
224519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
224524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
224526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
224526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.1ns 
224527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
226933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
227716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
227721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
227722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
227722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
227723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
230127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
230910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
230916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
230917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
230917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
230918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
233323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
234109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
234113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
234114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
234115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
234115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
236522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
237308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
237310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 758.61ns 
237311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
237312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
237312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
239715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
240501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
240505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
240506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
240507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
240507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
242916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
243699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
243703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
243705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
243705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.41ns 
243706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
246113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
246905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
246965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.4ms 
246968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
246968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.41ns 
246969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
249391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
250177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
250217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.06ms 
250219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
250219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
250220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
252635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
253423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
253455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.47ms 
253456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
253456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
253457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
255867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
256652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
256699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.07ms 
256702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
256702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.21ns 
256703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
259113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
259899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
259931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.53ms 
259934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
259934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.8ns 
259935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
262348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
263133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
263185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.14ms 
263187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
263188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.71ns 
263188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
265600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
266384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
266413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.97ms 
266414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
266414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
266415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
268821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
269602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
269623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.66ms 
269624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
269624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
269625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
272031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
272818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
272843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.48ms 
272846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
272847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.11ns 
272848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
275252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
276038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
276059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.46ms 
276060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
276060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
276061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
278479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
279262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
279292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.91ms 
279293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
279293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
279294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
281735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
282519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
282546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.3ms 
282547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
282547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
282548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
284963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
285750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
285777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.12ms 
285778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
285778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
285779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
288188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
288973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
288999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.04ms 
289001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
289001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
289002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
291410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
292193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
292216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.69ms 
292217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
292217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
292218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
294630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
295414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
295439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.41ms 
295440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
295441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
295441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
297839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
298623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
298649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.97ms 
298650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
298650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
298651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
301055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
301849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
301857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ms 
301858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
301858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
301859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
304268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
305054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
305072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.33ms 
305074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
305074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
305074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
307480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
308264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
308268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
308269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
308269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
308270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
310680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
311466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
311469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 729.41ns 
311470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
311470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
311471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
313875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
314665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
314667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 873.71ns 
314669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
314669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
314670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
317084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
317876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
317889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.14ms 
317890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
317890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
317891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
320315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
321081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
321088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
321090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
321090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.7ns 
321091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
323520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
324278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
324290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.13ms 
324292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
324292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
324292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
326707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
327469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
327472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
327474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
327474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
327475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
329887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
330645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
330647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.61ns 
330649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
330649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
330649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
333068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
333826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
333832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
333833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
333834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
333835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
336251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
337009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
337011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 668.62ns 
337013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
337013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
337013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
339434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
340203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
340205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.21ns 
340206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
340206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
340207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
342647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
343411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
343414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.21ns 
343415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
343415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
343416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
345856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
346619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
346624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
346625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
346625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
346626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
349072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
349834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
349844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.44ms 
349846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
349846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
349846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
352282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
353044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
353048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
353049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
353049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
353050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
355485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
356249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
356256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
356257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
356257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
356258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
358679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
359443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
359451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.1ms 
359456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
359457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.91ns 
359460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
361900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
362664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
362681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.68ms 
362682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
362682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
362683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
365138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
365903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
365907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
365909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
365909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
365909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
368359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
369126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
369130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
369131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
369131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
369132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
371582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
372347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
372351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
372352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
372352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
372353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
374776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
375568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
375586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.01ms 
375589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
375589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.5ns 
375590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
378019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
378809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
378814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.21ns 
378817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
378817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.1ns 
378818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
381207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
381985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
382025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.09ms 
382027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
382027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
382027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
384416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
385199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
385203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
385204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
385204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
385205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
387613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
388408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
388431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.31ms 
388435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
388435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.41ns 
388436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
390868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
391656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
391677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.25ms 
391679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
391679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
391680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
394109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
394899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
394925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.75ms 
394927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
394927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
394928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
397346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
398139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
398142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 646.11ns 
398143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
398143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
398144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
400555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
401340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
401346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
401347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
401347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
401348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
403752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
404541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
404545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
404546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
404546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
404547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
406951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
407738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
407741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 971.02ns 
407742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
407743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
407743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
410157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
410948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
410951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.02ns 
410955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
410955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.5ns 
410956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
413367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
414157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
414161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
414162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
414162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
414163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
416582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
417373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
417376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
417377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
417377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
417378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
419797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
420587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
420597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ms 
420599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
420599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
420600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
423017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
423811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
423823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.23ms 
423824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
423824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
423825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
426230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
427036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
427050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.72ms 
427053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
427053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
427054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
429465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
430261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
430274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.74ms 
430276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
430276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.7ns 
430277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
432685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
433480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
433484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
433486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
433486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
433487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
435886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
436678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
436684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
436685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
436685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
436686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
439074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
439864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
439867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 739.91ns 
439868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
439868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
439869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
442253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
443047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
443050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
443051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
443051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
443052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
445450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
446243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
446246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 953.12ns 
446247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
446247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
446248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
448678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
449482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
449494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 
449497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
449497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.4ns 
449498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
451978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
452747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
452751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
452752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
452752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
452753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
455178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
455945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
455952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
455953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
455953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
455954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
458365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
459133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
459135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 865.12ns 
459136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
459137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
459137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
461552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
462352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
462354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.99ns 
462355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
462355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
462356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
464745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
465537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
465541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
465543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
465543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
465543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
467943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
468739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
468742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
468744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
468744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
468744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
471142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
471937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
471940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
471942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
471942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
471942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
474328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
475124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
475127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
475128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
475128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
475129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
477517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
478308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
478313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
478314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
478314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
478315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
480726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
481523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
481526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
481528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
481528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
481528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
483979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
484750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
484762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
484764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
484764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.1ns 
484765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
487190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
487984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
487987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 710.91ns 
487988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
487988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
487989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
490403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
491198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
491205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
491206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
491206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
491207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
493620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
494413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
494415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 992.82ns 
494417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
494417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
494418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
496828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
497622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
497624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 862.52ns 
497625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
497625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
497626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
500037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
500807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
500812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
500813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
500813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
500814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
503247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
504018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
504021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
504022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
504022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
504023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
506436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
507228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
507232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
507233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
507233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
507234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
509623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
510419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
510423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
510425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
510425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
510425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
512824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
513617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
513622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
513623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
513623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
513624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
516039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
516806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
516821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.69ms 
516822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
516822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
516823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
519237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
520031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
520047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.26ms 
520048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
520048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
520049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
522448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
523243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
523253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ms 
523255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
523255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
523256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
525659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
526457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
526468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
526469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
526469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
526470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
528900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
529669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
529695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.78ms 
529697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
529697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
529697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
532115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
532915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
532940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.38ms 
532942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
532942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
532943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
535345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
536139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
536163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21ms 
536164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
536164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
536165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
538597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
539365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
539379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ms 
539380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
539380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
539381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
541791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
542585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
542618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.95ms 
542620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
542620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
542621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
545029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
545820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
545867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.77ms 
545869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
545869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
545869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
548281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
549054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
549093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.81ms 
549094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
549094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
549095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
551516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
552313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
552356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.3ms 
552357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
552357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
552358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
554785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
555585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
555629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.85ms 
555631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
555631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
555632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
558059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
558852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
558972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.25ms 
558973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
558974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
558974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
561388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
562185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
562193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.89ms 
562195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
562195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
562195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
564619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
565388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
565396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.04ms 
565398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
565398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
565398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
567814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
568609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
568614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
568616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
568616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
568617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
571013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
571809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
571827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.92ms 
571828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
571828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
571829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
574239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
575031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
575043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.17ms 
575044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
575044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
575045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
577438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
578231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
578234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
578236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
578236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
578236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
580651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
581447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
581466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.11ms 
581468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
581468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
581468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
583873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
584668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
584685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
584687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
584687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
584687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
587111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
587883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
587903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.03ms 
587905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
587905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
587905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
590327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
591120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
591123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
591124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
591125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
591125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
593551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
594323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
594327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
594328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
594328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
594329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
596738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
597528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
597534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
597535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
597535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
597536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
599956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
600731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
600740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.77ms 
600742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
600742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232ns 
600743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
603176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
603970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
604043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.9ms 
604044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
604045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
604045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
606479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
607248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
607275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.44ms 
607277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
607277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
607278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
609685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
610478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
610501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.49ms 
610502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
610503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
610503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
612913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
613706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
613708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 320.01ns 
613709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
613709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
613710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
616101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
616893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
617092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 188.76ms 
617097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
617097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.41ns 
617098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
619521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
620317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
620367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.46ms 
620369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
620369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
620369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
622810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
623581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
623583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 417.31ns 
623585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
623585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
623585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
626007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
626801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
626803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 404.41ns 
626805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
626805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
626806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
629230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
630023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
630025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 386.91ns 
630027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
630027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
630027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
632420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
633215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
633217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 554.41ns 
633218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
633218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
633219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
635624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
636416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
636504     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
636522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.51ms 
636525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
636525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.7ns 
636526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
638960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
639758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
639817     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
639818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.44ms 
639819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
639819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
639821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
642236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
643043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
643045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
643070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
643119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
643136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
643140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
643146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
643149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
643150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
643152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
643154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
643156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
643158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
643159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
643392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
643394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
643395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
643396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
643397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
643507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
643508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
643509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
643511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
643512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
643513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
643668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
643670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
643672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
643672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
643673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
643674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
643794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
643796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
643797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
643798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
643799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
643799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
643806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
643807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
643807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
643809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
643810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
643811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
643817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
643818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
643819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
643820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
643821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
643822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
643960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
643961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
643963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
644085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
644087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
644089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
644090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
644091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
644092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
644093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
644094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
644098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
644100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
644101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
644102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
644103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
644214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
644218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
644220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
644221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
644222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
644222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
644223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
644399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
644401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
644402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
644405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
644406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
644407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
644408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
644409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
644513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
644515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
644639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
644644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
644650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
644652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
644655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
644656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
644658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
644658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
644659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
644660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
644670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
644676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
644795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
644797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
644799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
644800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
644801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
644801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
644803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
644806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
644869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
644875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
644982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
644984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
644986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
644988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
644989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
644990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
645157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
645162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
645165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
645167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
645168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
645170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
645171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
645172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
645184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
645189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
645191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
645192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
645319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
645321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
645322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
645323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
645324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
645325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
645442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
645443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
645444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
645446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
645447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
645448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
645448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
645449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
645539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
645541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
645626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
645627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
645628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
645634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
645638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
645642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
645791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
645792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
645793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
645795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
645807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
645898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
649555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
649556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
649562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
649563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
649564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
649565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
649565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
649574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
649575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
649577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
649578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
649632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
649730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
649735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
649737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
649737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
649738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
649738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
649744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
649845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
649846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
649847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
649848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
649849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
649850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
649850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
649852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
649932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
649934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
650013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
650017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
650022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
650023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
650024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
650024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
650035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
650122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
650123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
650124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
650125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
650200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
650210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
650210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
650212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
650213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
650214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
650214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
650215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
650226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
650227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
650228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
650229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
650229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
650321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
650323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
650324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
650325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
650325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
650425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
650430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
650432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
650432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
650433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
650434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
650435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
650537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
650539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
650540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
650541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
650542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
650542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
650543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
650544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
650545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
650545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
650547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
650547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
650548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
650548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
650549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
650641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
650643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
650649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
650732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
650818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
650820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
650821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
650822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
650823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
650823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
650824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
650824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
650825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
650916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
650923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
651019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
651021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
651022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
651023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
651024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
651024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
651024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
651025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
651031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
651032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
651116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
651121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
651127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
651234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
651235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
651236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
651237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
651237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
651238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
651238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
651239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
651296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
651297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
651298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
651299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
651300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
651307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
651314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
651439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
651532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
651534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
651535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
651536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
651711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
651849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
651850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
655107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
655112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
655114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
655115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
655115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
655236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
655238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
655239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
655240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
655241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
655351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
658606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
661964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
661969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
661970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
661971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
661972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
662091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
662093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
662094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
662095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
662097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
663340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
663341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 
663341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
665873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
666702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
666703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ns 
666704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
666713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
666724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
666726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
666728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
666729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
666733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
666735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
666738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
666741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
666742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
666751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
666753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
666754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
666803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
666804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
666804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
666805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
666806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
666876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
666876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
666878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
666879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
666879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
666883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
666884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
666884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
666886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
666886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
666887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
666972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
666973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
666973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
666975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
666976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
666977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
667066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
667067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
667068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
667069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
667069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
667071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
667071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
667072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
667073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
667073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
667074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
667074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
667075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
667075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
667076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
667076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
667077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
667078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
667079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
667082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
667116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
667117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
667171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
667172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
667174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
667175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
667176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
667176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
667221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
667223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
667225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
667226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
667228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
667229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
667229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
667272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
667274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
667278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
667330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
667383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
667383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
667384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
669823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
670637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
670668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.64ms