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

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

tests
0

failures
0

ignored
10m9.07s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.081s passed
powPositiveConcrete data()[101] 2.935s passed
powGeq1Concrete data()[102] 2.811s passed
pow2InIntLower data()[103] 2.979s passed
pow2InIntUpper data()[104] 3.082s passed
logSelfConcrete data()[105] 3.081s passed
log1Concrete data()[106] 2.972s passed
logProduct data()[107] 2.993s passed
logTimesBaseConcrete data()[108] 3.073s passed
logProdIdentity data()[109] 2.971s passed
moduloByteIsInByte data()[10] 3.137s passed
logProdIdentityConcrete data()[110] 3.071s passed
logPowIdentity data()[111] 3.012s passed
logPowIdentityConcrete data()[112] 2.765s passed
logPositive data()[113] 2.897s passed
logPositiveConcrete data()[114] 2.966s passed
logMono data()[115] 2.937s passed
logMonoConcrete data()[116] 2.752s passed
powLogLess data()[117] 2.922s passed
powLogMore2 data()[118] 3.005s passed
logLessThanPow data()[119] 3.084s passed
moduloCharIsInChar data()[11] 3.127s passed
logLessThanPowConcrete data()[120] 2.804s passed
logSqueeze data()[121] 2.740s passed
ifthenelse_equals data()[122] 2.741s passed
ifthenelse_equals_1 data()[123] 2.740s passed
ifthenelse_equals_2 data()[124] 3.008s passed
disjointWithSingleton1 data()[125] 3.078s passed
disjointWithSingleton2 data()[126] 3.079s passed
disjointArrayRanges data()[127] 2.884s passed
disjointArrayRangeAllFields1 data()[128] 2.923s passed
disjointArrayRangeAllFields2 data()[129] 2.835s passed
div_unique1 data()[12] 3.159s passed
seqSelfDefinition data()[130] 3.040s passed
seqOutsideValue data()[131] 2.915s passed
castedGetAny data()[132] 2.793s passed
seqGetAlphaCast data()[133] 2.823s passed
getOfSeqSingleton data()[134] 2.760s passed
getOfSeqSingletonConcrete data()[135] 2.775s passed
getOfSeqConcat data()[136] 2.866s passed
getOfSeqSub data()[137] 3.049s passed
getOfSeqReverse data()[138] 2.874s passed
lenOfSeqEmpty data()[139] 2.907s passed
div_unique2 data()[13] 3.062s passed
lenOfSeqSingleton data()[140] 2.752s passed
lenOfSeqConcat data()[141] 2.860s passed
lenOfSeqSub data()[142] 2.767s passed
lenOfSeqReverse data()[143] 2.998s passed
equalityToSeqGetAndSeqLenLeft data()[144] 2.855s passed
equalityToSeqGetAndSeqLenRight data()[145] 2.784s passed
getOfSeqSingletonEQ data()[146] 2.746s passed
getOfSeqConcatEQ data()[147] 2.744s passed
getOfSeqSubEQ data()[148] 2.738s passed
getOfSeqReverseEQ data()[149] 2.839s passed
div_exists data()[14] 3.198s passed
lenOfSeqEmptyEQ data()[150] 3.107s passed
lenOfSeqSingletonEQ data()[151] 3.082s passed
lenOfSeqConcatEQ data()[152] 2.975s passed
lenOfSeqSubEQ data()[153] 3.013s passed
lenOfSeqReverseEQ data()[154] 3.067s passed
getOfSeqDefEQ data()[155] 3.061s passed
lenOfSeqDefEQ data()[156] 2.893s passed
seqConcatWithSeqEmpty1 data()[157] 2.888s passed
seqConcatWithSeqEmpty2 data()[158] 2.999s passed
seqReverseOfSeqEmpty data()[159] 3.050s passed
div_one data()[15] 3.119s passed
subSeqComplete data()[160] 3.092s passed
subSeqTailR data()[161] 3.104s passed
subSeqTailL data()[162] 3.128s passed
subSeqTailEQR data()[163] 3.104s passed
subSeqTailEQL data()[164] 3.121s passed
seqDef_split data()[165] 3.138s passed
seqDef_induction_upper data()[166] 3.138s passed
seqDef_induction_upper_concrete data()[167] 3.033s passed
seqDef_induction_lower data()[168] 3.039s passed
seqDef_induction_lower_concrete data()[169] 3.139s passed
jdiv_one data()[16] 2.987s passed
seqDef_split_in_three data()[170] 3.205s passed
seqDef_empty data()[171] 3.087s passed
seqDef_one_summand data()[172] 3.097s passed
seqDef_lower_equals_upper data()[173] 3.036s passed
seqDefOfSeq data()[174] 2.972s passed
seqSelfDefinitionEQ2 data()[175] 2.985s passed
indexOfSeqSingleton data()[176] 2.883s passed
indexOfSeqConcatFirst data()[177] 2.916s passed
indexOfSeqConcatSecond data()[178] 3.110s passed
indexOfSeqSub data()[179] 2.858s passed
div_zero data()[17] 2.990s passed
lenOfArray2seq data()[180] 3.064s passed
getAnyOfArray2seq data()[181] 3.079s passed
getOfArray2seq data()[182] 3.098s passed
getAnyOfNPermInv data()[183] 3.074s passed
seqNPermRange data()[184] 3.117s passed
seqPermTrans data()[185] 2.951s passed
seqPermRefl data()[186] 3.035s passed
seqPermSplit data()[187] 3.087s passed
seqNPermRight data()[188] 3.261s passed
seqPermFromSwap data()[189] 3.146s passed
divResZero1 data()[18] 2.797s passed
seqPermTransAlt0 data()[190] 3.085s passed
seqPermTransAlt1 data()[191] 2.827s passed
seqPermTransAlt2 data()[192] 3.093s passed
seqPermTransAlt3 data()[193] 3.090s passed
seqPermForall data()[194] 3.188s passed
seqPermExists data()[195] 2.906s passed
schiffl_lemma_2 data()[196] 21.253s passed
schiffl_thm_1 data()[197] 3.867s passed
eqSameSeq data()[198] 2.897s passed
divResZero2 data()[19] 2.794s passed
eqTermCut data()[1] 3.399s passed
divResOne1 data()[20] 2.903s passed
divResOne2 data()[21] 2.913s passed
div_cancel1 data()[22] 2.799s passed
div_cancel2 data()[23] 2.896s passed
divAddMultDenom data()[24] 2.942s passed
divMinus data()[25] 3.170s passed
divMinusDenom data()[26] 3.150s passed
divLeastDPos data()[27] 3.066s passed
divLeastDNeg data()[28] 3.149s passed
divGreatestDPos data()[29] 3.110s passed
equivAllRight data()[2] 3.172s passed
divGreatestDNeg data()[30] 2.996s passed
divIncreasingPos data()[31] 2.833s passed
divIncreasingNeg data()[32] 3.098s passed
jdiv_zero data()[33] 3.093s passed
jdivPulloutMinusNum data()[34] 3.097s passed
jdivPulloutMinusDenom data()[35] 3.160s passed
jdiv_uniquePosPos data()[36] 2.986s passed
jdiv_uniquePosNeg data()[37] 3.105s passed
jdiv_uniqueNegPos data()[38] 3.119s passed
jdiv_uniqueNegNeg data()[39] 3.125s passed
irrflConcrete1 data()[3] 3.329s passed
jdivMultDenom1 data()[40] 2.797s passed
jdivMultDenom2 data()[41] 2.852s passed
mod_geZero data()[42] 2.750s passed
mod_lessDenom data()[43] 2.757s passed
jmod_NumPos data()[44] 2.839s passed
jmod_NumNeg data()[45] 3.096s passed
jmod_geZero data()[46] 3.091s passed
jmodNumZero data()[47] 3.076s passed
jmod_pulloutminusNum data()[48] 3.092s passed
jmod_pulloutminusDenom data()[49] 3.027s passed
irrflConcrete2 data()[4] 3.164s passed
jmodUnique1 data()[50] 3.146s passed
jmodUnique2 data()[51] 3.165s passed
intDivRem data()[52] 3.088s passed
jmodjmod data()[53] 3.126s passed
jmodDivisible data()[54] 3.113s passed
jmodDivisibleRep data()[55] 3.087s passed
jdivAddMultDenom data()[56] 3.074s passed
jmodAltZero data()[57] 3.151s passed
jmodAddMultDenomZero data()[58] 3.083s passed
polyDiv_zero data()[59] 3.066s passed
cancel_gtPos data()[5] 2.946s passed
polyMod_ltdivDenom data()[60] 3.106s passed
bsum_empty data()[61] 3.072s passed
bsum_induction_upper data()[62] 2.972s passed
bsum_induction_lower data()[63] 3.108s passed
bsum_num_of_bounds data()[64] 2.938s passed
bsum_num_of_bounds2 data()[65] 2.882s passed
bsum_induction_upper2 data()[66] 2.748s passed
bsum_induction_upper_concrete data()[67] 2.806s passed
bsum_induction_upper_concrete_2 data()[68] 2.843s passed
bsum_induction_upper2_concrete data()[69] 2.764s passed
cancel_gtNeg data()[6] 3.206s passed
bsum_induction_lower_concrete data()[70] 2.866s passed
bsum_induction_lower2 data()[71] 2.863s passed
bsum_induction_lower2_concrete data()[72] 2.755s passed
bsum_positive data()[73] 2.804s passed
bsum_upper_bound data()[74] 2.957s passed
bsum_lower_bound data()[75] 2.838s passed
bsum_positive_lower_bound_element data()[76] 2.841s passed
bsum_sub_same_index data()[77] 2.775s passed
bsum_less_same_index data()[78] 2.789s passed
bsum_equal_except_one_index data()[79] 2.767s passed
moduloIntIsInInt data()[7] 3.161s passed
bsum_num_of_is_max data()[80] 2.855s passed
bsum_num_of_is_max2 data()[81] 2.761s passed
bsum_num_of_is_max3 data()[82] 2.756s passed
bsum_num_of_is_max4 data()[83] 2.931s passed
bsum_num_of_lt_max data()[84] 3.044s passed
bsum_num_of_lt_max2 data()[85] 2.772s passed
bsum_num_of_lt_max3 data()[86] 2.769s passed
bsum_num_of_lt_max4 data()[87] 2.761s passed
bsum_num_of_gt0 data()[88] 2.841s passed
bsum_num_of_gt0_alt data()[89] 3.066s passed
moduloLongIsInLong data()[8] 2.852s passed
bsum_add_concrete data()[90] 2.894s passed
bprod_all_positive data()[91] 2.974s passed
bprod_split data()[92] 2.981s passed
powConcrete0 data()[93] 3.083s passed
powConcrete1 data()[94] 3.079s passed
powSplitFactor data()[95] 2.808s passed
powAdd data()[96] 2.986s passed
powMono data()[97] 3.090s passed
powMonoConcrete data()[98] 2.913s passed
powMonoConcreteRight data()[99] 2.928s passed
moduloShortIsInShort data()[9] 2.957s passed

Standard output

362        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
388        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.74ms 
627        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645        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)

1542       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1544       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1546       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1546       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2794       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7613       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.99s 
7687       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7724       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.5ns 
7740       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7742       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.8ms 
7747       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10343      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
10345      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11101      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11129      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.71ms 
11138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.5ns 
11140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13524      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
13525      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
14295      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
14308      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.49ms 
14310      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
14310      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.8ns 
14311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
16802      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
17630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
17637      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
17640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
17641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.15ms 
17643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
19978      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
20789      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
20801      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.94ms 
20804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
20804      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 827.81ns 
20805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22957      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
22958      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
23670      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
23745      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.27ms 
23752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
23753      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 588.01ns 
23754      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26153      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
26154      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
26937      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
26955      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.46ms 
26958      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
26958      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.11ns 
26959      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29321      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
29322      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
30113      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
30116      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.31ns 
30119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
30119      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.2ns 
30120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
32268      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
32966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
32969      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 598.61ns 
32971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
32971      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120ns 
32972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35139      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
35139      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
35922      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
35925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.01ns 
35928      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
35929      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 733.71ns 
35930      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38282      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
38282      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
39059      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
39062      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 580.21ns 
39065      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
39065      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.8ns 
39066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41413      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
41414      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
42187      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
42190      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.81ns 
42192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
42192      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.61ns 
42194      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44537      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
44538      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
45310      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
45349      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.57ms 
45354      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
45355      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.12ms 
45357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47640      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
47640      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
48345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
48413      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.51ms 
48415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
48415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.6ns 
48419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50705      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
50706      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
51477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
51610      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 124.46ms 
51613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
51614      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.31ns 
51615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53954      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
53954      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
54725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
54730      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
54732      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
54733      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.7ns 
54734      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56969      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
56970      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
57715      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
57719      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
57720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
57720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.2ns 
57721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59906      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
59909      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
60651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
60708      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.87ms 
60711      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
60711      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.8ns 
60712      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.09s 
62807      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
63493      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
63507      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.33ms 
63509      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
63509      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.8ns 
63510      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65589      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.08s 
65589      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
66287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
66301      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.51ms 
66304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
66304      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.5ns 
66305      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68505      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
68505      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
69191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
69205      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.87ms 
69207      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
69207      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.9ns 
69208      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
71410      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
72104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
72117      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.84ms 
72119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
72120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.6ns 
72121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74204      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.08s 
74205      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
74895      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
74917      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.12ms 
74918      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
74918      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.8ns 
74919      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77089      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
77089      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
77808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
77812      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
77814      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
77814      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.4ns 
77816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79985      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
79985      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
80703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
80754      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.97ms 
80756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
80756      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.3ns 
80757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83097      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
83098      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
83866      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
83923      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.09ms 
83926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
83927      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.4ns 
83928      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86261      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
86261      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
87030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
87074      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.65ms 
87076      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
87077      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.41ns 
87078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
89411      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
90132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
90140      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.62ms 
90143      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
90143      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.9ns 
90144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92510      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
92510      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
93276      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
93289      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.27ms 
93290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
93290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
93291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95619      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
95619      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
96388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
96400      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.47ms 
96401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
96401      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.5ns 
96402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98702      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
98702      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
99389      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
99396      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.87ms 
99398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
99398      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.4ns 
99399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.09s 
101487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
102220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
102229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
102230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
102230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
102231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
104550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
105320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
105327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
105328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
105328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
105329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
107651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
108416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
108420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
108421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
108421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
108422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
110743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
111507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
111517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.96ms 
111519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
111519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.6ns 
111520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
113805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
114567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
114677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.11ms 
114679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
114679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns 
114680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
116900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
117647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
117664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.92ms 
117666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
117666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.8ns 
117667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
119985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
120752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
120769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.42ms 
120770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
120770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
120771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
123093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
123865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
123887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.6ms 
123890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
123891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.61ns 
123892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
126228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
126993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
127012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.53ms 
127015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
127015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.61ns 
127016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.07s 
129085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
129774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
129810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.57ms 
129813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
129813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.5ns 
129814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
131964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
132660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
132663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 965.81ns 
132664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
132664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
132665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
134726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
135409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
135413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
135414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
135415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
135415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
137479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
138163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
138170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.71ms 
138172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
138172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
138172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.14s 
140309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
140994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
141009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.77ms 
141012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
141012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 490.01ns 
141013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
143331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
144085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
144106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.98ms 
144107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
144107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
144108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
146425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
147189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
147197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.86ms 
147198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
147198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
147199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
149495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
150265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
150273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
150276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
150276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.1ns 
150277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
152597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
153361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
153365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
153366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
153366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
153367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
155625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
156388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
156392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
156394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
156394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
156394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
158707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
159468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
159538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.55ms 
159540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
159540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.6ns 
159541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
161862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
162624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
162703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.63ms 
162705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
162705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
162706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
165024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
165788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
165791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
165793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
165793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
165794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
168108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
168883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
168917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.53ms 
168919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
168919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.4ns 
168920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
171240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
172002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
172030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.79ms 
172032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
172032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
172032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
174346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
175114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
175117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
175118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
175118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
175120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
177356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
178038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
178190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 143.44ms 
178193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
178194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.1ns 
178195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
180565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
181331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
181343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
181344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
181344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.9ns 
181345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
183655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
184417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
184425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
184427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
184427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
184428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
186744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
187458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
187491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.02ms 
187493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
187493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
187493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
189821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
190583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
190596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.75ms 
190598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
190598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
190599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
192909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
193665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
193669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
193671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
193671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
193671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
195894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
196637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
196641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
196643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
196643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
196644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
198960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
199724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
199749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.47ms 
199750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
199751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
199751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
201987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
202673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
202688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ms 
202689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
202689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
202690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
204874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
205555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
205570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.97ms 
205571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
205571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
205572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
207635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
208315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
208318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
208319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
208319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
208320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
210381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
211119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
211123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
211125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
211125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
211125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
213273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
213962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
213967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
213968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
213968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
213969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.08s 
216045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
216728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
216731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
216732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
216732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
216733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
218888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
219595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
219598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 706.21ns 
219599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
219599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.9ns 
219600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
221777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
222458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
222461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
222463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
222463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
222464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
224521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
225214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
225217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 977.41ns 
225218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
225218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
225219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
227280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
227961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
228020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.54ms 
228023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
228023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.1ns 
228026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
230265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
230946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
230978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.03ms 
230980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
230980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
230980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.07s 
233046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
233785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
233816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.03ms 
233818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
233818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
233819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.07s 
235886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
236617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
236657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.67ms 
236659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
236659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
236660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
238722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
239406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
239433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.13ms 
239434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
239434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 
239435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
241497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
242178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
242222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.54ms 
242223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
242224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
242224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
244284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
244964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
244988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.67ms 
244989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
244989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
244990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
247138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
247826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
247843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.61ms 
247845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
247845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
247845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
249902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
250582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
250604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.84ms 
250605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
250605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
250606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
252666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
253344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
253361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.39ms 
253362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
253362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
253363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.14s 
255506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
256266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
256292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.65ms 
256294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
256294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
256295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
258600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
259314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
259336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.43ms 
259338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
259338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
259339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
261400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
262086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
262109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.31ms 
262110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
262110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
262111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
264175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
264855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
264877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.04ms 
264878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
264878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
264879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
266939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
267619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
267638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms 
267640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
267640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
267640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
269703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
270449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
270479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.16ms 
270481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
270481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.6ns 
270482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
272760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
273521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
273545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.64ms 
273547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
273547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
273548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
275752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
276433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
276440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
276441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
276441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.92ns 
276442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
278632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
279395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
279413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.32ms 
279415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
279415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
279416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
281629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
282391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
282395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
282396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
282396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
282397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
284713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
285475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
285477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.44ns 
285479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
285479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
285479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
287791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
288554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
288556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 818.21ns 
288557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
288558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
288558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.12s 
290677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
291357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
291364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
291367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
291367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.4ns 
291368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
293631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
294345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
294351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 
294352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
294352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
294353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
296667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
297429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
297441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.01ms 
297442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
297442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
297443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
299669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
300351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
300355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
300356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
300356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
300356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
302533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
303280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
303282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.41ns 
303284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
303284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
303284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
305597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
306358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
306364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
306365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
306365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
306366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
308614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
309297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
309299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 696.51ns 
309301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
309301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
309301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
311366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
312108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
312110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 600.71ns 
312112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
312113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.9ns 
312113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
314348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
315087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
315090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 681.71ns 
315092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
315092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.6ns 
315093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
317408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
318169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
318173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
318174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
318174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
318175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
320483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
321244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
321253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.06ms 
321254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
321255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
321255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
323482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
324221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
324225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
324227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
324227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
324227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
326447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
327212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
327219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
327220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
327220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
327221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
329526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
330287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
330292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
330293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
330293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
330294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
332487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
333247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
333263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.33ms 
333264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
333264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
333265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
335569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
336330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
336334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
336335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
336335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
336336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
338636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
339343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
339346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
339347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
339347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
339348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.08s 
341424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
342107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
342111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
342112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
342112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
342113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.13s 
344248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
344991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
345007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.17ms 
345009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
345009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196ns 
345010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
347255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
347968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
347973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 576.71ns 
347975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
347975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
347976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
350198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
350876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
350911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.71ms 
350912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
350912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
350913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
352975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
353660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
353664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
353665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
353665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
353666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.14s 
355804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
356564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
356585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.85ms 
356586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
356586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
356587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
358811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
359570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
359590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.94ms 
359592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
359592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
359592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
361891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
362650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
362674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.32ms 
362675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
362676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
362676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.12s 
364795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
365476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
365478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 519.01ns 
365480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
365480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
365480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.05s 
367533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
368214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
368219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
368220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
368220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
368221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.05s 
370274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
370957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
370960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
370961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
370961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
370962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.05s 
373014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
373697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
373699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 820.01ns 
373701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
373701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
373701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
375941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
376705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
376708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 859.81ns 
376709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
376709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
376710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
379016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
379783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
379786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
379787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
379787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
379788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
382095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
382862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
382864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
382866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
382866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
382867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.13s 
385001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
385739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
385749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ms 
385751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
385751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
385751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
387982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
388662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
388672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.84ms 
388674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
388674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
388674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.13s 
390802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
391495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
391507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.68ms 
391510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
391510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
391511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
393816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
394529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
394548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms 
394549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
394549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.9ns 
394550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
396768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
397459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
397463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
397464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
397464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
397465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.1s 
399564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
400251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
400256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.96ms 
400258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
400258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
400258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.05s 
402308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
403077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
403079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 746.11ns 
403081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
403081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
403081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.08s 
405165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
405836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
405839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
405840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
405840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
405841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.1s 
407941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
408612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
408614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 824.31ns 
408615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
408616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
408616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.1s 
410719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
411470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
411480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.86ms 
411482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
411482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
411482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
413745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
414524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
414529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
414531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
414531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.8ns 
414532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
416704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
417397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
417404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
417405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
417405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
417406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
419618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
420310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
420312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 704.01ns 
420313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
420313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
420314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
422371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
423063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
423065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 638.01ns 
423066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
423066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
423067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.13s 
425199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
425921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
425924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
425926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
425926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.8ns 
425926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.07s 
427993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
428689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
428692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
428693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
428693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
428693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
431016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
431686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
431689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
431690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
431690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
431691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
433874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
434542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
434545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
434546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
434546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
434547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.09s 
436634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
437324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
437329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
437331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
437331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
437331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.05s 
439386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
440073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
440076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
440077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
440077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
440077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.04s 
442120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
442809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
442819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.79ms 
442820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
442820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
442821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.05s 
444867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
445556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
445558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 642.21ns 
445559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
445559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
445560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.08s 
447636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
448390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
448398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.46ms 
448399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
448399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
448400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
450724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
451501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
451504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
451506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
451506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.9ns 
451507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
453813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
454584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
454587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 789.81ns 
454588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
454588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
454588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
456813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
457557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
457562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
457563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
457563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
457563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
459802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
460571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
460574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
460575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
460575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
460576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
462889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
463638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
463641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
463643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
463643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
463643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
465958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
466699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
466702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
466705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
466705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
466705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.11s 
468820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
469592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
469597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
469598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
469598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
469599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.12s 
471722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
472472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
472485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.91ms 
472487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
472487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
472487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
474702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
475469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
475484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.09ms 
475486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
475486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
475486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
477751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
478524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
478534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
478535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
478535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
478536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
480840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
481615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
481626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.71ms 
481627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
481627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
481628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
483954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
484706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
484731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.77ms 
484732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
484732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
484733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
487059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
487834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
487858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.09ms 
487859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
487859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
487860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
490162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
490939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
490962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.97ms 
490964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
490964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
490965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
493291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
494069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
494083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.88ms 
494084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
494085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
494085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
496392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
497168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
497221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.8ms 
497226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
497226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.2ns 
497227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
499535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
500316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
500362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.45ms 
500364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
500364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
500365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
502658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
503357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
503395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.5ms 
503398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
503398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.1ns 
503399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
505638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
506393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
506434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.43ms 
506435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
506436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
506436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
508757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
509530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
509573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.02ms 
509575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
509575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
509576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
511891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
512663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
512778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.91ms 
512780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
512780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
512781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
515108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
515857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
515865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.76ms 
515866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
515867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
515867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
518184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
518955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
518963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.68ms 
518964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
518964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
518965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
521285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
521991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
521998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
521999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
521999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
522000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
524262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
524950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
524970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.6ms 
524971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
524971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
524972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
527180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
527943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
527955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.16ms 
527957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
527957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
527957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
530147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
530836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
530839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
530840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
530840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
530840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.13s 
532968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
533738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
533754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.62ms 
533756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
533756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
533756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
536077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
536848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
536864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.61ms 
536865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
536865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
536866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
539017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
539705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
539722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.41ms 
539723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
539723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
539724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
542012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
542783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
542786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
542787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
542787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
542788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
545089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
545862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
545865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
545866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
545867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
545867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
548186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
548957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
548963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
548965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
548965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
548965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
551261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
552031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
552037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
552039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
552039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
552039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
554356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
555096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
555154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.08ms 
555156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
555156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
555157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
557329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
558080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
558105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.52ms 
558107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
558108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218ns 
558108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
560340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
561117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
561140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.34ms 
561142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
561142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
561142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
563455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
564226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
564227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 288.8ns 
564229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
564229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
564230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
566531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
567301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
567488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 177.08ms 
567490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
567491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.5ns 
567492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
569818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
570591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
570634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.47ms 
570636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
570636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
570636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
572947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
573717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
573719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 363.51ns 
573724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
573724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.9ns 
573725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.06s 
575781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
576545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
576547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 366.81ns 
576549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
576549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
576549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
578866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
579639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
579641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 397.01ns 
579642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
579642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
579643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
581958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
582728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
582730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 528.91ns 
582732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
582732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
582732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
585031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
585803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
585918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.84ms 
585920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
585920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.9ns 
585923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.11s 
588035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
588768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
588825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.68ms 
588826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
588826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
588832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.08s 
590911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
591605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
591607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
591630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
591662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
591676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
591679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
591684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
591686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
591686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
591688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
591690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
591692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
591694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
591695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
591864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
591866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
591868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
591869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
591870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
591997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
591998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
591999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
592001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
592002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
592003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
592164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
592166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
592167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
592168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
592169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
592170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
592289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
592291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
592292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
592293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
592294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
592295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
592301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
592302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
592303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
592305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
592306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
592307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
592313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
592314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
592314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
592315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
592316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
592317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
592463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
592464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
592466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
592597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
592598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
592601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
592602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
592603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
592604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
592604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
592605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
592608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
592610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
592612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
592612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
592613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
592720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
592724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
592725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
592726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
592727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
592727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
592728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
592835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
592836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
592837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
592839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
592839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
592840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
592841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
592842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
592928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
592930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
593015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
593019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
593023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
593024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
593025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
593026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
593027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
593028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
593028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
593029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
593037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
593041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
593135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
593136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
593137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
593138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
593139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
593140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
593140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
593141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
593192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
593197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
593291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
593293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
593295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
593296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
593297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
593298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
593431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
593435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
593436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
593438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
593440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
593440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
593441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
593442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
593451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
593452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
593453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
593454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
593550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
593552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
593553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
593554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
593555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
593555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
593657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
593659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
593660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
593661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
593662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
593663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
593663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
593665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
593744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
593746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
593818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
593818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
593819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
593824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
593828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
593832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
593950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
593952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
593953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
593954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
593963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
594047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
597458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
597459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
597463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
597464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
597465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
597465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
597466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
597474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
597475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
597476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
597476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
597477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
597561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
597565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
597566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
597567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
597567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
597568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
597569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
597653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
597655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
597656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
597658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
597659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
597659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
597660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
597661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
597729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
597730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
597797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
597801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
597805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
597806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
597807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
597808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
597817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
597888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
597889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
597889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
597890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
597954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
597963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
597963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
597965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
597966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
597966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
597967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
597967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
597977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
597978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
597979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
597979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
597980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
598057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
598059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
598060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
598060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
598061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
598141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
598145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
598147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
598147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
598148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
598148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
598149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
598236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
598238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
598238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
598240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
598240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
598241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
598241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
598242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
598243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
598243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
598244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
598245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
598245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
598246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
598246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
598324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
598326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
598331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
598401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
598515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
598517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
598518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
598519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
598522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
598522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
598523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
598525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
598526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
598601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
598607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
598685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
598686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
598687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
598688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
598688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
598689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
598689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
598690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
598694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
598695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
598765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
598769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
598774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
598862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
598863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
598864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
598865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
598865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
598865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
598866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
598866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
598915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
598915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
598916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
598917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
598917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
598922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
598927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
599029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
599107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
599108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
599109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
599110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
599258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
599337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
599337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
602349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
602354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
602355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
602356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
602357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
602471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
602472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
602473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
602473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
602474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
602579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
605588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
608804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
608808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
608809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
608810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
608810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
608922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
608924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
608925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
608925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
608927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
610078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
610079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
610079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
612470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
613225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
613226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
613226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
613232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
613243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
613245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
613246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
613247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
613251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
613252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
613254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
613256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
613257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
613265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
613266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
613267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
613357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
613357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
613358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
613359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
613359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
613424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
613425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
613426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
613427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
613427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
613431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
613431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
613432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
613433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
613433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
613434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
613512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
613513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
613514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
613515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
613516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
613516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
613601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
613601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
613602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
613603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
613603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
613604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
613605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
613605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
613606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
613607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
613607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
613608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
613608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
613609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
613609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
613610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
613610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
613611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
613612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
613615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
613653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
613654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
613715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
613716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
613718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
613719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
613719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
613720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
613775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
613778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
613779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
613780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
613781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
613782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
613782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
613836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
613839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
613842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
613894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
613947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
613947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.2ns 
613948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.14s 
616090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
616815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
616842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.17ms