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

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
198

tests
0

failures
0

ignored
13m0.52s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.834s passed
powPositiveConcrete data()[101] 3.796s passed
powGeq1Concrete data()[102] 3.759s passed
pow2InIntLower data()[103] 3.779s passed
pow2InIntUpper data()[104] 3.750s passed
logSelfConcrete data()[105] 3.749s passed
log1Concrete data()[106] 3.755s passed
logProduct data()[107] 3.783s passed
logTimesBaseConcrete data()[108] 3.762s passed
logProdIdentity data()[109] 3.802s passed
moduloByteIsInByte data()[10] 3.923s passed
logProdIdentityConcrete data()[110] 3.770s passed
logPowIdentity data()[111] 3.810s passed
logPowIdentityConcrete data()[112] 3.804s passed
logPositive data()[113] 3.809s passed
logPositiveConcrete data()[114] 3.781s passed
logMono data()[115] 3.807s passed
logMonoConcrete data()[116] 3.761s passed
powLogLess data()[117] 3.820s passed
powLogMore2 data()[118] 3.791s passed
logLessThanPow data()[119] 3.798s passed
moduloCharIsInChar data()[11] 3.889s passed
logLessThanPowConcrete data()[120] 3.794s passed
logSqueeze data()[121] 3.770s passed
ifthenelse_equals data()[122] 3.835s passed
ifthenelse_equals_1 data()[123] 3.786s passed
ifthenelse_equals_2 data()[124] 3.804s passed
disjointWithSingleton1 data()[125] 3.770s passed
disjointWithSingleton2 data()[126] 3.784s passed
disjointArrayRanges data()[127] 3.768s passed
disjointArrayRangeAllFields1 data()[128] 3.784s passed
disjointArrayRangeAllFields2 data()[129] 3.777s passed
div_unique1 data()[12] 3.863s passed
seqSelfDefinition data()[130] 3.800s passed
seqOutsideValue data()[131] 3.781s passed
castedGetAny data()[132] 3.771s passed
seqGetAlphaCast data()[133] 3.786s passed
getOfSeqSingleton data()[134] 3.817s passed
getOfSeqSingletonConcrete data()[135] 3.800s passed
getOfSeqConcat data()[136] 3.862s passed
getOfSeqSub data()[137] 3.798s passed
getOfSeqReverse data()[138] 3.787s passed
lenOfSeqEmpty data()[139] 3.837s passed
div_unique2 data()[13] 3.980s passed
lenOfSeqSingleton data()[140] 3.831s passed
lenOfSeqConcat data()[141] 3.774s passed
lenOfSeqSub data()[142] 3.797s passed
lenOfSeqReverse data()[143] 3.787s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.753s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.793s passed
getOfSeqSingletonEQ data()[146] 3.773s passed
getOfSeqConcatEQ data()[147] 3.778s passed
getOfSeqSubEQ data()[148] 3.861s passed
getOfSeqReverseEQ data()[149] 3.795s passed
div_exists data()[14] 4.018s passed
lenOfSeqEmptyEQ data()[150] 3.790s passed
lenOfSeqSingletonEQ data()[151] 3.815s passed
lenOfSeqConcatEQ data()[152] 3.812s passed
lenOfSeqSubEQ data()[153] 3.784s passed
lenOfSeqReverseEQ data()[154] 3.774s passed
getOfSeqDefEQ data()[155] 3.791s passed
lenOfSeqDefEQ data()[156] 3.799s passed
seqConcatWithSeqEmpty1 data()[157] 3.804s passed
seqConcatWithSeqEmpty2 data()[158] 3.811s passed
seqReverseOfSeqEmpty data()[159] 3.798s passed
div_one data()[15] 3.859s passed
subSeqComplete data()[160] 3.818s passed
subSeqTailR data()[161] 3.770s passed
subSeqTailL data()[162] 3.812s passed
subSeqTailEQR data()[163] 3.798s passed
subSeqTailEQL data()[164] 3.816s passed
seqDef_split data()[165] 3.811s passed
seqDef_induction_upper data()[166] 3.814s passed
seqDef_induction_upper_concrete data()[167] 3.855s passed
seqDef_induction_lower data()[168] 3.803s passed
seqDef_induction_lower_concrete data()[169] 3.859s passed
jdiv_one data()[16] 3.819s passed
seqDef_split_in_three data()[170] 3.840s passed
seqDef_empty data()[171] 3.801s passed
seqDef_one_summand data()[172] 3.806s passed
seqDef_lower_equals_upper data()[173] 3.780s passed
seqDefOfSeq data()[174] 3.795s passed
seqSelfDefinitionEQ2 data()[175] 3.786s passed
indexOfSeqSingleton data()[176] 3.826s passed
indexOfSeqConcatFirst data()[177] 3.806s passed
indexOfSeqConcatSecond data()[178] 3.886s passed
indexOfSeqSub data()[179] 3.787s passed
div_zero data()[17] 3.831s passed
lenOfArray2seq data()[180] 3.800s passed
getAnyOfArray2seq data()[181] 3.790s passed
getOfArray2seq data()[182] 3.785s passed
getAnyOfNPermInv data()[183] 3.753s passed
seqNPermRange data()[184] 3.915s passed
seqPermTrans data()[185] 3.851s passed
seqPermRefl data()[186] 3.843s passed
seqPermSplit data()[187] 3.849s passed
seqNPermRight data()[188] 3.892s passed
seqPermFromSwap data()[189] 3.833s passed
divResZero1 data()[18] 3.863s passed
seqPermTransAlt0 data()[190] 3.806s passed
seqPermTransAlt1 data()[191] 3.775s passed
seqPermTransAlt2 data()[192] 3.786s passed
seqPermTransAlt3 data()[193] 3.807s passed
seqPermForall data()[194] 3.996s passed
seqPermExists data()[195] 3.879s passed
schiffl_lemma_2 data()[196] 26.520s passed
schiffl_thm_1 data()[197] 4.795s passed
eqSameSeq data()[198] 3.870s passed
divResZero2 data()[19] 3.815s passed
eqTermCut data()[1] 4.656s passed
divResOne1 data()[20] 3.771s passed
divResOne2 data()[21] 3.776s passed
div_cancel1 data()[22] 3.792s passed
div_cancel2 data()[23] 3.773s passed
divAddMultDenom data()[24] 3.845s passed
divMinus data()[25] 3.812s passed
divMinusDenom data()[26] 3.827s passed
divLeastDPos data()[27] 3.915s passed
divLeastDNeg data()[28] 3.821s passed
divGreatestDPos data()[29] 3.868s passed
equivAllRight data()[2] 4.442s passed
divGreatestDNeg data()[30] 3.830s passed
divIncreasingPos data()[31] 3.820s passed
divIncreasingNeg data()[32] 3.839s passed
jdiv_zero data()[33] 3.800s passed
jdivPulloutMinusNum data()[34] 3.813s passed
jdivPulloutMinusDenom data()[35] 3.849s passed
jdiv_uniquePosPos data()[36] 3.804s passed
jdiv_uniquePosNeg data()[37] 3.813s passed
jdiv_uniqueNegPos data()[38] 3.815s passed
jdiv_uniqueNegNeg data()[39] 3.776s passed
irrflConcrete1 data()[3] 4.259s passed
jdivMultDenom1 data()[40] 3.898s passed
jdivMultDenom2 data()[41] 3.757s passed
mod_geZero data()[42] 3.798s passed
mod_lessDenom data()[43] 3.849s passed
jmod_NumPos data()[44] 3.845s passed
jmod_NumNeg data()[45] 3.784s passed
jmod_geZero data()[46] 3.827s passed
jmodNumZero data()[47] 3.805s passed
jmod_pulloutminusNum data()[48] 3.854s passed
jmod_pulloutminusDenom data()[49] 3.784s passed
irrflConcrete2 data()[4] 4.038s passed
jmodUnique1 data()[50] 3.840s passed
jmodUnique2 data()[51] 3.881s passed
intDivRem data()[52] 3.926s passed
jmodjmod data()[53] 3.789s passed
jmodDivisible data()[54] 3.782s passed
jmodDivisibleRep data()[55] 3.756s passed
jdivAddMultDenom data()[56] 3.916s passed
jmodAltZero data()[57] 3.830s passed
jmodAddMultDenomZero data()[58] 3.737s passed
polyDiv_zero data()[59] 3.782s passed
cancel_gtPos data()[5] 4.000s passed
polyMod_ltdivDenom data()[60] 3.751s passed
bsum_empty data()[61] 3.737s passed
bsum_induction_upper data()[62] 3.741s passed
bsum_induction_lower data()[63] 3.781s passed
bsum_num_of_bounds data()[64] 3.851s passed
bsum_num_of_bounds2 data()[65] 3.793s passed
bsum_induction_upper2 data()[66] 3.847s passed
bsum_induction_upper_concrete data()[67] 3.768s passed
bsum_induction_upper_concrete_2 data()[68] 3.807s passed
bsum_induction_upper2_concrete data()[69] 3.771s passed
cancel_gtNeg data()[6] 3.914s passed
bsum_induction_lower_concrete data()[70] 3.759s passed
bsum_induction_lower2 data()[71] 3.782s passed
bsum_induction_lower2_concrete data()[72] 3.802s passed
bsum_positive data()[73] 3.797s passed
bsum_upper_bound data()[74] 3.850s passed
bsum_lower_bound data()[75] 3.859s passed
bsum_positive_lower_bound_element data()[76] 3.815s passed
bsum_sub_same_index data()[77] 3.803s passed
bsum_less_same_index data()[78] 3.815s passed
bsum_equal_except_one_index data()[79] 3.764s passed
moduloIntIsInInt data()[7] 3.910s passed
bsum_num_of_is_max data()[80] 3.751s passed
bsum_num_of_is_max2 data()[81] 3.812s passed
bsum_num_of_is_max3 data()[82] 3.752s passed
bsum_num_of_is_max4 data()[83] 3.842s passed
bsum_num_of_lt_max data()[84] 3.810s passed
bsum_num_of_lt_max2 data()[85] 3.765s passed
bsum_num_of_lt_max3 data()[86] 3.790s passed
bsum_num_of_lt_max4 data()[87] 3.864s passed
bsum_num_of_gt0 data()[88] 3.759s passed
bsum_num_of_gt0_alt data()[89] 3.754s passed
moduloLongIsInLong data()[8] 3.857s passed
bsum_add_concrete data()[90] 3.736s passed
bprod_all_positive data()[91] 3.739s passed
bprod_split data()[92] 3.898s passed
powConcrete0 data()[93] 3.734s passed
powConcrete1 data()[94] 3.749s passed
powSplitFactor data()[95] 3.853s passed
powAdd data()[96] 3.764s passed
powMono data()[97] 3.789s passed
powMonoConcrete data()[98] 3.772s passed
powMonoConcreteRight data()[99] 3.746s passed
moduloShortIsInShort data()[9] 3.849s passed

Standard output

464        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
497        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.56ms 
772        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
800        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)

1854       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1857       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1862       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1863       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3372       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9714       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.94s 
9800       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9845       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.1ns 
9871       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9871       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.3ns 
9884       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13360      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
13363      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14472      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14505      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.12ms 
14519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14520      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.1ns 
14524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17816      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
17817      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18942      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
18959      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ms 
18964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
18965      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 682.31ns 
18967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
22144      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
23205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
23217      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
23224      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23225      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.31ns 
23227      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26224      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
26225      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
27247      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
27259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.58ms 
27263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
27264      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.03ms 
27267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
30237      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
31219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
31261      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.3ms 
31264      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
31265      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 657.91ns 
31266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34179      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
34179      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
35152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
35176      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.3ms 
35178      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
35178      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.2ns 
35183      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38124      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
38124      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
39081      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
39085      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 809.81ns 
39090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
39090      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415.31ns 
39092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42010      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
42010      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
42941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
42944      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.11ns 
42947      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
42948      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364ns 
42950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45859      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
45860      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
46791      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
46794      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.81ns 
46797      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
46798      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.61ns 
46799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49705      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
49705      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
50707      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
50717      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
50721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
50722      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414ns 
50724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53645      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
53645      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
54604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
54607      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 689.01ns 
54610      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
54611      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 423.4ns 
54612      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57468      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
57469      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
58430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
58470      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.99ms 
58484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
58485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 604.41ns 
58487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61471      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
61472      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
62425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
62459      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30ms 
62462      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
62463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.7ns 
62464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65383      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
65384      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
66356      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
66476      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.04ms 
66480      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
66481      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.2ns 
66482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69316      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
69316      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
70332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
70337      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
70340      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
70341      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.5ns 
70342      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73212      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
73213      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
74152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
74157      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
74159      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
74160      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.4ns 
74161      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77030      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
77032      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
77948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
77988      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.38ms 
77990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
77991      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.7ns 
77992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80868      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
80868      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
81822      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
81850      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.36ms 
81854      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
81854      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 584.41ns 
81856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84713      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
84714      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
85655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
85667      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.31ms 
85669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
85670      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240ns 
85671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88482      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
88483      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
89424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
89437      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
89440      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
89440      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.11ns 
89442      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92257      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
92258      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
93201      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
93214      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.78ms 
93217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
93217      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.5ns 
93218      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96041      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
96042      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
96985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
97005      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.72ms 
97008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
97008      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394ns 
97010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99830      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
99830      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
100771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
100778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
100781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
100782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.9ns 
100783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
103663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
104579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
104623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.31ms 
104626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
104627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.6ns 
104628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
107467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
108384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
108436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.85ms 
108439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
108439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.4ns 
108440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
111288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
112228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
112263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.29ms 
112265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
112265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.7ns 
112266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
115187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
116157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
116175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.96ms 
116183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
116184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.18ms 
116186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
119035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
119985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
120001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.86ms 
120010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
120010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 701.91ns 
120012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
122898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
123864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
123875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.82ms 
123877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
123877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.3ns 
123878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
126706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
127696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
127705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
127708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
127708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.2ns 
127709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
130559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
131515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
131524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.26ms 
131527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
131527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.4ns 
131529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
134441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
135356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
135364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
135366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
135367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.5ns 
135368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
138242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
139159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
139163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
139166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
139167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.2ns 
139168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
142047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
142963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
142977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.43ms 
142980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
142980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.3ns 
142982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
145841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
146783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
146825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.72ms 
146829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
146829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.11ns 
146830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
149665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
150611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
150630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.23ms 
150633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
150634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.7ns 
150635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
153477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
154421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
154444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.3ms 
154445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
154446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.1ns 
154447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
157277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
158235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
158259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.54ms 
158260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
158261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.5ns 
158262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
161073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
162014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
162035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ms 
162037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
162037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.7ns 
162038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
164956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
165894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
165933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.06ms 
165935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
165935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.5ns 
165936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
168775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
169687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
169691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
169692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
169692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.3ns 
169693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
172565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
173483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
173488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
173490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
173491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 508.91ns 
173492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
176371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
177327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
177337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ms 
177339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
177339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.7ns 
177340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
180211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
181174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
181183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ms 
181184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
181184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
181185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
184002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
184943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
184966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.89ms 
184967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
184967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.7ns 
184968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
187835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
188781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
188793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.07ms 
188795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
188795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.3ns 
188796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
191650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
192595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
192599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
192600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
192600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
192601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
195508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
196448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
196452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
196454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
196454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.5ns 
196455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
199316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
200232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
200236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
200238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
200238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
200239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
203080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
204012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
204076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.03ms 
204078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
204078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.7ns 
204079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
206929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
207875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
207957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.64ms 
207959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
207959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.5ns 
207960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
210937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
211880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
211883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
211885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
211886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.6ns 
211887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
214698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
215638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
215672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.59ms 
215675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
215675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 459.31ns 
215676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
218486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
219428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
219453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.4ms 
219457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
219457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.7ns 
219458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
222268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
223207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
223210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
223211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
223212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
223213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
226049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
226997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
227126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 115.98ms 
227130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
227130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.7ns 
227131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
229990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
230947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
230958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.01ms 
230960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
230961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.2ns 
230962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
233780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
234685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
234695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
234696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
234696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
234697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
237521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
238459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
238477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.82ms 
238478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
238478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
238479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
241280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
242215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
242228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
242230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
242230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
242231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
245028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
245962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
245965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
245967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
245967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
245968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
248767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
249702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
249706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
249707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
249708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
249708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
252509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
253467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
253487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.8ms 
253489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
253489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133ns 
253490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
256358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
257317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
257337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.97ms 
257345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
257346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.1ns 
257347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
260211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
261122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
261136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.39ms 
261138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
261138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
261139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
264042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
264979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
264983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
264985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
264985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
264986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
267836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
268747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
268751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
268752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
268752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
268753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
271605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
272552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
272558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
272560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
272560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
272561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
275394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
276326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
276329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
276330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
276330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
276331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
279149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
280086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
280088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 690.11ns 
280089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
280089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
280090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
282911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
283866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
283871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
283872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
283872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
283873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
286723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
287670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
287673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 878.61ns 
287674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
287674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
287675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
290488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
291430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
291469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.26ms 
291471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
291472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.2ns 
291473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
294335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
295263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
295319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.1ms 
295321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
295321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.3ns 
295322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
298242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
299148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
299178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.37ms 
299181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
299181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns 
299182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
301997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
302947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
302993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.89ms 
302995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
302995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115ns 
302996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
305840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
306775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
306796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.75ms 
306798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
306798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
306799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
309630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
310570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
310611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.93ms 
310613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
310613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
310613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
313422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
314354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
314375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.39ms 
314377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
314377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
314378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
317175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
318109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
318126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.41ms 
318127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
318127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
318128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
320973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
321914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
321937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.55ms 
321943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
321943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.1ns 
321944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
324764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
325673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
325693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.46ms 
325694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
325695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.6ns 
325695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
328602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
329509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
329535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.52ms 
329538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
329538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.1ns 
329539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
332373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
333326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
333345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.59ms 
333346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
333347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 
333347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
336154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
337090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
337110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.84ms 
337111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
337111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85ns 
337112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
339911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
340873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
340892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.52ms 
340902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
340902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125ns 
340903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
343781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
344747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
344764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms 
344765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
344765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
344766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
347562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
348502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
348523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.92ms 
348526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
348526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.1ns 
348527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
351325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
352258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
352277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.79ms 
352279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
352279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.8ns 
352280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
355104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
356007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
356013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
356015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
356015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
356016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
358831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
359738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
359752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.72ms 
359754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
359754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.8ns 
359755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
362708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
363645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
363650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
363651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
363651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
363652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
366447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
367382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
367384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.11ns 
367386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
367386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
367386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
370188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
371131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
371134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 758.61ns 
371135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
371135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
371136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
373973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
374970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
374984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.78ms 
374989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
374989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.2ns 
374991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
377812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
378746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
378752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.75ms 
378753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
378753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
378754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
381590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
382529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
382541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.79ms 
382542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
382542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
382543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
385391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
386308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
386312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
386313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
386314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
386314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
389147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
390055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
390058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 600.81ns 
390059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
390059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
390060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
392898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
393886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
393892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
393894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
393894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.5ns 
393895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
396742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
397686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
397688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 621.71ns 
397690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
397690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
397691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
400505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
401445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
401447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.21ns 
401449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
401449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
401450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
404283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
405224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
405226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 561.81ns 
405229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
405229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.7ns 
405230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
408033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
408973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
408977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
408978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
408978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
408979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
411768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
412717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
412725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.36ms 
412726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
412726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
412727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
415539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
416477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
416480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
416482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
416482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
416482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
419346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
420257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
420264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
420265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
420265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
420266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
423110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
424021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
424026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
424027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
424027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.5ns 
424028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
426867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
427814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
427827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.99ms 
427829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
427829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
427830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
430640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
431590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
431597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
431600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
431601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.2ns 
431602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
434462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
435405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
435408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
435410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
435410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.1ns 
435411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
438236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
439209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
439213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
439214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
439214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
439215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
442020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
443005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
443020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ms 
443023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
443033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.04ms 
443034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
445858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
446797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
446802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 432.5ns 
446804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
446804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
446813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
449647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
450578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
450609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.53ms 
450611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
450611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
450612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
453452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
454366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
454370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
454372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
454372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
454372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
457233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
458173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
458191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.49ms 
458192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
458192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
458193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
461025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
461965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
461982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.69ms 
461983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
461983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
461984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
464821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
465758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
465779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.61ms 
465780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
465781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
465781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
468617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
469570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
469573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 554.21ns 
469575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
469576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243ns 
469577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
472398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
473338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
473344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
473345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
473345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
473346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
476254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
477174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
477178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
477180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
477180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.3ns 
477181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
480038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
480961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
480964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 883.61ns 
480966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
480966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
480967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
483827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
484767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
484770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 793.81ns 
484771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
484771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
484772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
487584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
488536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
488539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
488541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
488541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
488541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
491378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
492320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
492323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
492325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
492325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
492326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
495126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
496082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
496091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.45ms 
496092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
496093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
496093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
498952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
499868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
499875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.03ms 
499876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
499876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
499877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
502702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
503645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
503652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
503653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
503653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
503654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
506487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
507444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
507452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.96ms 
507454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
507454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.5ns 
507455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
510270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
511229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
511233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
511234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
511234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
511235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
514072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
515000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
515004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
515006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
515006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
515007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
517836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
518788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
518790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 785.41ns 
518792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
518792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
518792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
521605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
522604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
522607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
522608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
522608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
522609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
525449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
526405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
526407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 942.61ns 
526409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
526409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
526410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
529298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
530258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
530269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.83ms 
530271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
530271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.2ns 
530272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
533112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
534064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
534067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
534068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
534068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
534069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
536891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
537847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
537854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
537856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
537856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235ns 
537857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
540759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
541688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
541691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 993.81ns 
541693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
541693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.8ns 
541693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
544565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
545520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
545522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.21ns 
545524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
545524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
545525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
548345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
549293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
549296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
549298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
549298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.8ns 
549298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
552147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
553091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
553094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 897.11ns 
553095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
553095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
553096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
555924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
556877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
556880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
556882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
556882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
556882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
559679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
560630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
560633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
560634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
560634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
560635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
563468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
564422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
564426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
564427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
564428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
564428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
567242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
568197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
568200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 943.81ns 
568201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
568201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
568202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
571039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
571968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
571977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.35ms 
571979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
571979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
571980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
574858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
575836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
575838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.41ns 
575840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
575840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
575841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
578665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
579625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
579633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
579635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
579635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
579636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
582468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
583420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
583423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 877.71ns 
583424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
583424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
583425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
586238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
587235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
587238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 775.61ns 
587239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
587240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
587240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
590090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
591046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
591050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
591052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
591052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
591052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
593879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
594832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
594835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 966.51ns 
594836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
594836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
594837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
597678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
598605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
598608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
598609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
598610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
598610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
601444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
602396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
602399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
602400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
602401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
602401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
605249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
606194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
606198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
606200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
606200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
606201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
609039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
609994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
610003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.23ms 
610004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
610004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
610005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
612861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
613805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
613814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.63ms 
613815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
613815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
613816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
616651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
617605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
617611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
617613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
617613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
617613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
620469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
621422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
621429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.99ms 
621430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
621431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85ns 
621431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
624236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
625187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
625199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.26ms 
625200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
625200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
625201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
628042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
629000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
629011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.02ms 
629012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
629012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
629013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
631832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
632792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
632809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.24ms 
632811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
632811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
632811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
635649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
636613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
636625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.06ms 
636626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
636626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
636627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
639485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
640414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
640436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.81ms 
640438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
640438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
640439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
643273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
644226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
644250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.55ms 
644252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
644252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
644253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
647132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
648083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
648105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.19ms 
648106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
648106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
648107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
650927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
651876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
651908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.14ms 
651910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
651910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
651911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
654784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
655745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
655767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.58ms 
655768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
655768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
655769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
658595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
659553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
659607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.24ms 
659609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
659609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
659610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
662448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
663403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
663408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms 
663410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
663410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
663410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
666256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
667208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
667214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
667215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
667215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
667216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
670040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
670990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
670994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
670996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
670996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
670996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
673849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
674774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
674789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.42ms 
674790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
674790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
674791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
677616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
678568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
678575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
678577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
678577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
678578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
681446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
682398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
682401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
682403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
682403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
682403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
685243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
686196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
686207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.74ms 
686209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
686209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
686210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
689123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
690081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
690093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
690095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
690095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
690096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
692918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
693865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
693880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.17ms 
693881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
693882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
693882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
696710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
697677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
697680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
697682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
697682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
697683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
700508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
701467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
701470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
701472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
701472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
701473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
704288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
705249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
705255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
705257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
705257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
705258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
708053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
709003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
709009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
709010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
709010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
709011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
711917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
712874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
712923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.69ms 
712925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
712925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
712926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
715801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
716753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
716774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.86ms 
716775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
716775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
716776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
719607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
720603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
720617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.18ms 
720619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
720619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
720619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
723503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
724465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
724467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 185ns 
724468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
724468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
724470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
727313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
728265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
728358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.61ms 
728360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
728360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
728361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
731191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
732152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
732192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.08ms 
732193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
732193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
732194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
735027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
735995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
735997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 392.11ns 
735999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
735999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
736000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
738842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
739770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
739772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 240ns 
739773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
739774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
739774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
742604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
743557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
743559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 239.6ns 
743560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
743560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
743561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
746408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
747363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
747365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 383.2ns 
747367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
747367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
747367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
750246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
751209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
751351     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
751361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 149.25ms 
751364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
751365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.2ns 
751366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
754230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
755191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
755240     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
755242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.6ms 
755243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
755243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
755244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
758088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
759053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
759055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
759089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
759127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
759143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
759149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
759161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
759163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
759166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
759167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
759173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
759175     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' 
759177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
759180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
759430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
759431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
759432     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' 
759433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
759434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
759559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
759560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
759561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
759562     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' 
759564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
759565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
759755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
759757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
759758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
759759     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' 
759760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
759761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
759903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
759904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
759906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
759907     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' 
759907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
759909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
759917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
759918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
759920     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' 
759921     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' 
759922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
759923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
759931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
759932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
759933     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' 
759934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
759935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
759936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
760091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
760092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
760093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
760314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
760315     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)'' 
760316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
760318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
760319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
760320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
760321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
760322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
760326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
760327     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' 
760328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
760330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
760330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
760466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
760471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
760473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
760474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
760475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
760476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
760477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
760622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
760623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
760625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
760626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
760627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
760628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
760628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
760629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
760748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
760749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
760860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
760865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
760871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
760872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
760873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
760874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
760875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
760876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
760876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
760877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
760887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
760892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
761020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
761021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
761022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
761024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
761024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
761025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
761026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
761026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
761095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
761104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
761245     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]'' 
761246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
761247     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'' 
761249     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'' 
761250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
761251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
761429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
761434     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'' 
761435     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)'' 
761436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
761438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
761439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
761439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
761440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
761452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
761453     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'' 
761454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
761456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
761586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
761587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
761589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
761590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
761590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
761591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
761731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
761733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
761734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
761735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
761736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
761737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
761737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
761744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
761870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
761871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
761985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
761986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
761986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
761992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
761998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
762004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
762184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
762186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
762187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
762188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
762200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
762311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
767088     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'' 
767088     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)'' 
767093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
767095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
767096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
767096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
767098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
767107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
767108     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'' 
767109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
767110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
767111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
767221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
767225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
767226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
767227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
767228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
767228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
767229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
767345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
767346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
767347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
767349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
767352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
767352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
767353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
767354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
767451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
767452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
767550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
767555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
767560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
767561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
767563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
767564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
767579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
767687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
767688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
767690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
767691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
767783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
767795     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'' 
767797     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)'' 
767798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
767799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
767800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
767801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
767802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
767815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
767816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
767817     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'' 
767818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
767819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
767924     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))'' 
767925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
767927     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'' 
767928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
767929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
768040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
768046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
768047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
768048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
768048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
768049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
768050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
768170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
768172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
768173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
768174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
768175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
768176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
768177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
768177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
768178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
768179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
768180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
768181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
768182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
768182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
768183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
768283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
768284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
768292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
768381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
768474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
768476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
768477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
768478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
768479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
768480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
768480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
768481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
768481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
768650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
768657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
768759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
768760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
768761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
768762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
768763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
768764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
768764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
768765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
768771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
768772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
768863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
768869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
768876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
768990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
768991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
768992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
768993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
768994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
768995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
768995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
768996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
769059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
769060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
769061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
769062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
769063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
769070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
769076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
769210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
769312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
769313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
769314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
769315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
769509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
769613     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'' 
769614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
773113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
773119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
773120     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'' 
773121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
773122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
773253     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))'' 
773254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
773255     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'' 
773255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
773256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
773376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
776676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
780317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
780321     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'' 
780322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
780323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
780324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
780456     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))'' 
780457     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'' 
780458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
780459     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)' ...' 
780459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
781762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
781763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
781763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
784690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
785683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
785684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
785685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
785692     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)'' 
785703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
785705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
785708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
785709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
785715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
785715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
785719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
785720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
785722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
785733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
785734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
785735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
785790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
785791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
785791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
785792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
785792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
785871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
785872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
785872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
785873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
785874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
785878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
785879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
785880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
785880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
785881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
785882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
785977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
785978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
785979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
785980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
785981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
785982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
786084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
786085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
786086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
786087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
786087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
786088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
786089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
786089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
786090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
786091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
786091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
786092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
786093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
786093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
786094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
786094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
786095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
786096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
786096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
786100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
786146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
786148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
786295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
786296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
786296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
786297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
786298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
786299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
786361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
786364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
786365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
786367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
786368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
786370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
786370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
786429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
786432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
786436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
786499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
786559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
786559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258ns 
786560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
789417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
790407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
790426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.89ms