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

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

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

398        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
424        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.23ms 
618        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630        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)

1543       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1547       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1551       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1551       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2896       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8047       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.43s 
8119       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8153       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.5ns 
8165       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8167       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.42ms 
8172       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11075      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
11077      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12011      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.57ms 
12021      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12021      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.8ns 
12022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14744      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
14745      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15644      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.83ms 
15647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15647      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.5ns 
15649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18279      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
18280      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19166      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ms 
19171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19171      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.8ns 
19173      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21715      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
21715      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22555      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
22557      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.3ns 
22558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25076      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
25076      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25958      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.03ms 
25962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25962      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.1ns 
25963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28458      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
28458      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29271      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29288      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.12ms 
29291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29291      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.5ns 
29292      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31825      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
31825      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32644      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.4ns 
32647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32647      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.1ns 
32648      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35139      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
35139      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35952      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35955      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 550.7ns 
35962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35963      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 549.3ns 
35964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38441      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
38442      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39261      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 558.1ns 
39264      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39264      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.6ns 
39265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41746      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
41747      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42547      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
42550      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42550      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.9ns 
42552      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45044      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
45045      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45852      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 530ns 
45855      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333ns 
45856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48305      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
48305      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49147      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.9ms 
49149      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49149      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.4ns 
49150      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51709      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
51709      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52560      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.44ms 
52564      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 576ns 
52566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55028      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
55028      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55975      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 139.96ms 
55980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55980      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.5ns 
55981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58446      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
58447      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59311      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
59313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59314      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.1ns 
59315      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
61772      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62579      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
62587      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62587      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.4ns 
62589      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65036      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
65036      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65863      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.76ms 
65865      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65865      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.7ns 
65866      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68324      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
68325      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69124      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69135      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.02ms 
69136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69136      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.3ns 
69137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71569      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
71569      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72364      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
72374      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.65ms 
72376      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
72376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
72377      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74824      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
74824      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
75599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
75610      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
75612      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
75612      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325ns 
75613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78060      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
78060      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78860      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
78883      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.84ms 
78889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
78891      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.21ms 
78892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81327      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
81327      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82123      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82138      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.98ms 
82139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82140      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.3ns 
82140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84588      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
84589      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
85382      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
85384      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
85386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
85386      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 
85387      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87835      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
87835      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
88634      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
88691      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.68ms 
88696      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
88697      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.8ns 
88698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91166      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
91166      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
91941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
92013      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.94ms 
92014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92014      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
92015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
94449      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
95244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95276      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.42ms 
95278      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95278      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.9ns 
95279      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97726      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
97726      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
98504      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
98513      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ms 
98514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
98514      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
98515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
100963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
101753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
101765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
101766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
101766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
101767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
104194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
104984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
104993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.35ms 
104995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
104995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115ns 
104996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
107437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
108235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
108242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
108243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
108244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
110664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
111456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
111462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms 
111464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
111464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
111465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
113901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
114676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
114682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
114683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
114683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.4ns 
114684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
117153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
117949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
117952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
117953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
117954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
117954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
120371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
121163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
121172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.44ms 
121173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
121174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
123614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
124390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
124434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.02ms 
124444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
124444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.5ns 
124446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
126957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
127748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
127763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ms 
127765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
127766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.6ns 
127769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
130184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
130975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
130989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.28ms 
130990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
130990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
130991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
133423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
134217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
134235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms 
134238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
134238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268ns 
134239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
136661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
137453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
137467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.57ms 
137469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
137469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
137470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
139911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
140681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
140733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.76ms 
140735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
140735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
140735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
143151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
143943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
143949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
143952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
143952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.6ns 
143955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
146396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
147169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
147172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
147174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
147174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
147174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
149606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
150392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
150399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
150400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
150400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
150401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
152816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
153616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
153623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ms 
153624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
153624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
153625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
156066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
156839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
156864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.32ms 
156873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
156873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.9ns 
156874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
159311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
160100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
160107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms 
160108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
160108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
160109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
162518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
163329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
163332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
163334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
163334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.8ns 
163336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
165759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
166546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
166550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
166551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
166551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
166552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
168972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
169760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
169764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
169765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
169765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
169766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
172192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
172960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
173010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.03ms 
173012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
173012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
173013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
175449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
176238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
176297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.89ms 
176299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
176299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
176299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
178718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
179488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
179491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 986.3ns 
179493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
179493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.4ns 
179494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
181919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
182704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
182733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.27ms 
182735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
182735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350ns 
182736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
185145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
185930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
185949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.81ms 
185950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
185950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
185951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
188377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
189168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
189171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 927.8ns 
189172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
189172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
189173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
191573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
192359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
192451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.27ms 
192452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
192453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.5ns 
192453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
194885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
195662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
195672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
195674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
195674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.3ns 
195677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
198110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
198899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
198904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
198906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
198906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
198906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
201312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
202099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
202113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.01ms 
202114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
202114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
202115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
204534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
205319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
205328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.98ms 
205330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
205330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
205331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
207739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
208521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
208524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
208525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
208525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
208525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
210941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
211708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
211712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
211713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
211713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
211713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
214131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
214918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
214931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.41ms 
214932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
214933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
214933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
217338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
218152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
218162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.09ms 
218163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
218164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
218164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
220583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
221371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
221382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.23ms 
221383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
221383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
221384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
223783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
224572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
224575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 956.4ns 
224578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
224578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.9ns 
224581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
227004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
227809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
227812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
227813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
227813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
227814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
230354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
231181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
231185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
231186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
231186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
231187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
233715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
234553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
234556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 886.6ns 
234557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
234557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
234558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
237100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
237905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
237907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 441ns 
237908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
237908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
237909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
240456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
241285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
241288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
241289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
241289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
241290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
243772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
244566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
244568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 655.8ns 
244569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
244569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
244570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
247001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
247789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
247820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.15ms 
247832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
247832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.4ns 
247833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
250240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
251027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
251056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.79ms 
251058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
251058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.5ns 
251059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
253495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
254265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
254285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ms 
254287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
254287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
254287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
256723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
257512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
257540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.33ms 
257541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
257541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
257542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
259982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
260751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
260769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.04ms 
260770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
260770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
260771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
263202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
264012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
264047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.39ms 
264049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
264049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.8ns 
264050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
266460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
267247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
267266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.84ms 
267267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
267267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
267268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
269703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
270490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
270504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.65ms 
270505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
270505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
270506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
272916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
273705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
273721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
273722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
273722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
273723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
276162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
276931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
276944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.36ms 
276945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
276945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
276946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
279393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
280179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
280196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.52ms 
280197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
280197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
280198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
282614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
283403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
283419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.82ms 
283420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
283420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
283421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
285848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
286637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
286656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.12ms 
286658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
286658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
286658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
289064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
289850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
289865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.86ms 
289866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
289866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
289867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
292294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
293062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
293076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ms 
293077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
293077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
293078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
295499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
296284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
296298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.31ms 
296300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
296300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
296300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
298697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
299485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
299499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.79ms 
299500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
299500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
299501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
301927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
302712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
302717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
302718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
302719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
302719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
305134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
305921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
305932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
305933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
305933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
305934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
308355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
309123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
309126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
309127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
309128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
309128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
311546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
312332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
312334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 496.7ns 
312335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
312336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
312336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
314741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
315531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
315533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 620.8ns 
315534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
315534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
315534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
317951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
318737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
318742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
318744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
318744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
318744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
321157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
321947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
321952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
321953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
321953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
321954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
324379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
325151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
325160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
325161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
325161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
325162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
327578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
328370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
328373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
328374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
328374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
328374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
330776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
331567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
331568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 429.8ns 
331570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
331570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
331570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
333991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
334783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
334788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
334789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
334789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
334789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
337199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
337992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
337994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 471.5ns 
337995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
337995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
337996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
340410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
341180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
341182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 474ns 
341183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
341183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
341184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
343601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
344386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
344388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 458.3ns 
344389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
344389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
344389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
346792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
347579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
347583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
347584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
347584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
347585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
350008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
350798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
350805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.78ms 
350806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
350806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
350807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
353216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
354004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
354007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
354008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
354008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
354009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
356433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
357204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
357209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
357210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
357210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
357211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
359632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
360420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
360424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
360425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
360425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
360426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
362829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
363619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
363630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.78ms 
363631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
363631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
363632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
366050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
366837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
366840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
366841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
366841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
366842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
369248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
370038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
370041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.8ns 
370042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
370042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
370043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
372464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
373252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
373255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
373256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
373256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
373256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
375667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
376455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
376467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.49ms 
376468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
376468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
376469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
378884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
379668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
379672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 275.7ns 
379673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
379674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
379674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
382072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
382855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
382879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.94ms 
382880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
382880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
382881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
385296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
386082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
386084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
386086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
386086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
386086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
388487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
389275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
389288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.98ms 
389290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
389290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.5ns 
389291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
391710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
392497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
392513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms 
392515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
392515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.7ns 
392516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
394937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
395708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
395724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.54ms 
395725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
395725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
395726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
398139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
398928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
398930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 397.2ns 
398932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
398932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.1ns 
398933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
401353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
402121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
402125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
402127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
402127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
402127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
404542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
405332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
405335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
405336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
405336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
405337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
407756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
408547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
408549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720.2ns 
408550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
408550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
408551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
410955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
411746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
411748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 646.3ns 
411749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
411749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
411750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
414169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
414960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
414963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
414965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
414965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
414965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
417384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
418174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
418177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
418178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
418178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
418179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
420586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
421386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
421393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
421394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
421394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
421395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
423877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
424698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
424706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.01ms 
424712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
424712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
424713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
427134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
427930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
427936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
427937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
427937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
427938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
430342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
431138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
431145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
431146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
431146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
431147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
433565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
434366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
434370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
434371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
434371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
434372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
436797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
437592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
437596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
437597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
437597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
437598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
440003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
440798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
440800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 676.6ns 
440801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
440801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
440802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
443222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
444022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
444024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
444025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
444026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
444026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
446446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
447243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
447246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 779.1ns 
447247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
447248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.9ns 
447248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
449668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
450465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
450473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms 
450474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
450474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
450475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
452879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
453676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
453679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
453680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
453680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
453681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
456102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
456907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
456912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
456913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
456913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.1ns 
456914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
459331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
460129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
460131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.9ns 
460132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
460132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
460133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
462546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
463341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
463343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 550.3ns 
463344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
463344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
463345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
465762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
466558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
466561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
466562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
466562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
466562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
468980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
469759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
469761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 664.9ns 
469762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
469762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
469763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
472178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
472976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
472978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 875.5ns 
472979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
472979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
472980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
475391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
476188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
476191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 802.9ns 
476192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
476192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
476192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
478607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
479406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
479409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
479410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
479410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
479411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
481825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
482623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
482625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.3ns 
482626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
482626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
482626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
485041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
485838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
485846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ms 
485847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
485847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
485848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
488266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
489063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
489065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.8ns 
489066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
489066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
489066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
491476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
492272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
492277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
492278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
492278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
492279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
494700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
495500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
495502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 713ns 
495503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
495503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
495504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
497918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
498697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
498699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 641.6ns 
498700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
498700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
498701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
501134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
501912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
501915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
501916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
501917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
501917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
504338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
505135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
505137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.7ns 
505138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
505138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
505139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
507555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
508391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
508394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
508396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
508396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
508396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
510807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
511604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
511606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.5ns 
511607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
511607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns 
511608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
514035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
514832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
514836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
514837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
514837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
514837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
517270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
518048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
518055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
518056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
518056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
518056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
520495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
521278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
521309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
521311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
521311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.2ns 
521312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
523728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
524531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
524536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
524537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
524537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
524538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
526953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
527753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
527759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
527760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
527760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
527760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
530173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
530987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
530997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.56ms 
530998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
530998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
530999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
533425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
534227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
534237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.26ms 
534238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
534238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
534238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
536650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
537450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
537459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.62ms 
537460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
537460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
537461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
539877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
540678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
540684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.52ms 
540686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
540686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.6ns 
540686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
543097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
543900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
543920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.04ms 
543922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
543922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.6ns 
543923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
546347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
547150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
547169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.35ms 
547171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
547171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
547171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
549615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
550418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
550436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.29ms 
550437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
550437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
550438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
552848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
553651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
553667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.61ms 
553669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
553669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
553669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
556079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
556880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
556897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
556898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
556898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
556899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
559313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
560117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
560160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.67ms 
560162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
560162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
560163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
562595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
563403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
563407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
563408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
563408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
563409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
565829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
566632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
566637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
566638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
566638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
566638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
569053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
569855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
569858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
569859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
569859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
569859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
572275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
573077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
573091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
573092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
573092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
573093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
575521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
576322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
576327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
576329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
576329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
576329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
578746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
579547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
579550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
579551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
579551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
579552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
581961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
582762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
582771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.83ms 
582772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
582772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
582772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
585198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
585997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
586007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.16ms 
586008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
586008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
586008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
588423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
589227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
589239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.41ms 
589240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
589240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
589240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
591649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
592450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
592452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 864.1ns 
592453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
592453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
592454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
594880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
595682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
595685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
595686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
595686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
595687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
598092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
598892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
598897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
598898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
598898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
598898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
601325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
602126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
602130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms 
602131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
602131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
602132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
604541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
605342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
605381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.77ms 
605383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
605383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
605383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
607811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
608611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
608627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.28ms 
608628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
608628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
608629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
611045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
611847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
611857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
611859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
611859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
611859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
614266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
615087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
615089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 245.3ns 
615090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
615090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
615091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
617507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
618306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
618378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.18ms 
618380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
618380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
618381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
620807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
621609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
621638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.72ms 
621640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
621640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
621640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
624048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
624849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
624851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.7ns 
624852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
624852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
624853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
627281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
628084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
628086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 188.8ns 
628087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
628087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
628088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
630495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
631297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
631298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 190.8ns 
631299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
631299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
631300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
633729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
634530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
634531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 302.6ns 
634532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
634532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
634533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
636941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
637754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
637827     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
637834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.45ms 
637836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
637837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180ns 
637837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
640283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
641086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
641128     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
641129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.01ms 
641130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
641130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
641131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
643571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
644375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
644376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 
644402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
644438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
644450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
644454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
644462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
644463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
644465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
644466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
644469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
644471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
644472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
644474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
644663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
644664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
644667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
644668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
644669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
644808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
644809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
644813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
644814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
644815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
644818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
644982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
644984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
644985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
644986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
644986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
644989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
645111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
645114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
645115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
645116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
645117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
645118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
645127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
645127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
645130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
645131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
645133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
645134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
645143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
645144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
645148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
645148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
645150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
645151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
645278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
645280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
645281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
645399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
645400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
645401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
645403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
645404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
645405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
645407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
645408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
645412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
645413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
645415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
645416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
645416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
645522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
645526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
645527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
645528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
645529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
645530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
645534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
645659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
645660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
645661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
645663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
645664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
645665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
645666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
645667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
645777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
645778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
645872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
645876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
645880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
645881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
645882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
645883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
645884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
645884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
645885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
645886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
645893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
645898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
645997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
645998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
645999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
646000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
646001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
646001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
646002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
646002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
646053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
646059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
646185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
646186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
646187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
646189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
646190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
646191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
646333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
646337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
646338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
646338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
646340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
646340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
646341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
646341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
646351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
646352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
646353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
646353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
646444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
646445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
646446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
646446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
646447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
646448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
646544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
646545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
646547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
646547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
646548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
646549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
646549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
646550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
646628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
646629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
646702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
646703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
646703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
646707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
646711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
646715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
646830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
646831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
646832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
646833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
646847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
646932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
650403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
650403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
650407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
650409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
650409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
650411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
650412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
650419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
650420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
650421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
650422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
650422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
650510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
650513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
650514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
650515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
650516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
650516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
650517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
650608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
650609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
650610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
650611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
650612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
650612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
650613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
650613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
650685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
650686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
650759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
650763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
650767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
650767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
650768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
650769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
650779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
650861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
650862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
650863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
650864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
650937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
650946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
650947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
650947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
650949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
650949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
650950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
650950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
650961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
650962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
650963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
650963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
650964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
651052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
651053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
651054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
651055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
651056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
651142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
651146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
651147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
651148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
651149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
651149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
651150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
651242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
651243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
651244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
651245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
651246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
651246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
651247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
651247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
651248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
651249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
651250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
651251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
651251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
651252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
651252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
651378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
651379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
651385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
651456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
651530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
651531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
651532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
651533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
651534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
651534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
651535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
651535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
651536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
651615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
651621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
651704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
651705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
651706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
651707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
651707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
651708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
651708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
651709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
651714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
651714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
651788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
651793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
651798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
651890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
651890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
651891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
651892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
651893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
651893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
651894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
651894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
651945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
651946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
651946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
651947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
651947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
651953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
651957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
652065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
652146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
652147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
652147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
652148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
652303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
652387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
652387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
655943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
655947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
655948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
655949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
655950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
656055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
656056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
656057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
656058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
656059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
656156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
658890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
661842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
661845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
661846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
661847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
661848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
661953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
661954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
661955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
661956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
661956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
663031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
663031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
663032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
665502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
666324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
666326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
666326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
666332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
666341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
666343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
666345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
666347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
666351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
666351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
666355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
666355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
666357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
666366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
666366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
666368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
666412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
666413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
666414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
666414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
666414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
666480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
666480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
666480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
666481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
666482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
666485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
666486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
666486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
666486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
666487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
666488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
666572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
666573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
666573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
666574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
666574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
666575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
666669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
666670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
666670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
666670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
666671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
666671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
666672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
666672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
666673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
666673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
666673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
666674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
666674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
666674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
666675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
666675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
666675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
666676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
666676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
666679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
666718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
666719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
666781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
666782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
666783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
666784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
666785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
666785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
666842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
666844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
666844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
666845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
666846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
666847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
666848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
666903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
666905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
666908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
667018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
667069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
667069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
667069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
669547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
670397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
670412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.44ms