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

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

tests
0

failures
0

ignored
12m52.43s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.725s passed
powPositiveConcrete data()[101] 3.755s passed
powGeq1Concrete data()[102] 3.770s passed
pow2InIntLower data()[103] 3.761s passed
pow2InIntUpper data()[104] 3.792s passed
logSelfConcrete data()[105] 3.851s passed
log1Concrete data()[106] 3.806s passed
logProduct data()[107] 3.805s passed
logTimesBaseConcrete data()[108] 3.787s passed
logProdIdentity data()[109] 3.867s passed
moduloByteIsInByte data()[10] 3.818s passed
logProdIdentityConcrete data()[110] 3.777s passed
logPowIdentity data()[111] 3.850s passed
logPowIdentityConcrete data()[112] 3.817s passed
logPositive data()[113] 3.834s passed
logPositiveConcrete data()[114] 3.857s passed
logMono data()[115] 3.888s passed
logMonoConcrete data()[116] 3.801s passed
powLogLess data()[117] 3.853s passed
powLogMore2 data()[118] 3.843s passed
logLessThanPow data()[119] 3.779s passed
moduloCharIsInChar data()[11] 3.649s passed
logLessThanPowConcrete data()[120] 3.783s passed
logSqueeze data()[121] 3.823s passed
ifthenelse_equals data()[122] 3.886s passed
ifthenelse_equals_1 data()[123] 3.799s passed
ifthenelse_equals_2 data()[124] 3.783s passed
disjointWithSingleton1 data()[125] 3.808s passed
disjointWithSingleton2 data()[126] 3.803s passed
disjointArrayRanges data()[127] 3.775s passed
disjointArrayRangeAllFields1 data()[128] 3.775s passed
disjointArrayRangeAllFields2 data()[129] 3.736s passed
div_unique1 data()[12] 3.896s passed
seqSelfDefinition data()[130] 3.749s passed
seqOutsideValue data()[131] 3.683s passed
castedGetAny data()[132] 3.719s passed
seqGetAlphaCast data()[133] 3.733s passed
getOfSeqSingleton data()[134] 3.824s passed
getOfSeqSingletonConcrete data()[135] 3.768s passed
getOfSeqConcat data()[136] 3.779s passed
getOfSeqSub data()[137] 3.776s passed
getOfSeqReverse data()[138] 3.773s passed
lenOfSeqEmpty data()[139] 3.808s passed
div_unique2 data()[13] 3.721s passed
lenOfSeqSingleton data()[140] 3.813s passed
lenOfSeqConcat data()[141] 3.821s passed
lenOfSeqSub data()[142] 3.868s passed
lenOfSeqReverse data()[143] 3.824s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.741s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.870s passed
getOfSeqSingletonEQ data()[146] 3.824s passed
getOfSeqConcatEQ data()[147] 3.824s passed
getOfSeqSubEQ data()[148] 3.755s passed
getOfSeqReverseEQ data()[149] 3.814s passed
div_exists data()[14] 3.971s passed
lenOfSeqEmptyEQ data()[150] 3.840s passed
lenOfSeqSingletonEQ data()[151] 3.741s passed
lenOfSeqConcatEQ data()[152] 3.658s passed
lenOfSeqSubEQ data()[153] 3.689s passed
lenOfSeqReverseEQ data()[154] 3.698s passed
getOfSeqDefEQ data()[155] 3.616s passed
lenOfSeqDefEQ data()[156] 3.654s passed
seqConcatWithSeqEmpty1 data()[157] 3.727s passed
seqConcatWithSeqEmpty2 data()[158] 3.708s passed
seqReverseOfSeqEmpty data()[159] 3.645s passed
div_one data()[15] 3.877s passed
subSeqComplete data()[160] 3.716s passed
subSeqTailR data()[161] 3.714s passed
subSeqTailL data()[162] 3.642s passed
subSeqTailEQR data()[163] 3.734s passed
subSeqTailEQL data()[164] 3.704s passed
seqDef_split data()[165] 3.769s passed
seqDef_induction_upper data()[166] 3.735s passed
seqDef_induction_upper_concrete data()[167] 3.712s passed
seqDef_induction_lower data()[168] 3.557s passed
seqDef_induction_lower_concrete data()[169] 3.460s passed
jdiv_one data()[16] 3.845s passed
seqDef_split_in_three data()[170] 3.804s passed
seqDef_empty data()[171] 3.622s passed
seqDef_one_summand data()[172] 3.587s passed
seqDef_lower_equals_upper data()[173] 3.653s passed
seqDefOfSeq data()[174] 3.640s passed
seqSelfDefinitionEQ2 data()[175] 3.649s passed
indexOfSeqSingleton data()[176] 3.620s passed
indexOfSeqConcatFirst data()[177] 3.665s passed
indexOfSeqConcatSecond data()[178] 3.628s passed
indexOfSeqSub data()[179] 3.597s passed
div_zero data()[17] 4.040s passed
lenOfArray2seq data()[180] 3.502s passed
getAnyOfArray2seq data()[181] 3.592s passed
getOfArray2seq data()[182] 3.538s passed
getAnyOfNPermInv data()[183] 3.616s passed
seqNPermRange data()[184] 3.644s passed
seqPermTrans data()[185] 3.741s passed
seqPermRefl data()[186] 3.642s passed
seqPermSplit data()[187] 3.766s passed
seqNPermRight data()[188] 3.933s passed
seqPermFromSwap data()[189] 3.824s passed
divResZero1 data()[18] 4.052s passed
seqPermTransAlt0 data()[190] 3.768s passed
seqPermTransAlt1 data()[191] 3.803s passed
seqPermTransAlt2 data()[192] 3.747s passed
seqPermTransAlt3 data()[193] 3.846s passed
seqPermForall data()[194] 3.892s passed
seqPermExists data()[195] 3.916s passed
schiffl_lemma_2 data()[196] 26.564s passed
schiffl_thm_1 data()[197] 4.671s passed
eqSameSeq data()[198] 3.867s passed
divResZero2 data()[19] 3.973s passed
eqTermCut data()[1] 4.117s passed
divResOne1 data()[20] 4.107s passed
divResOne2 data()[21] 3.993s passed
div_cancel1 data()[22] 3.968s passed
div_cancel2 data()[23] 3.903s passed
divAddMultDenom data()[24] 4.050s passed
divMinus data()[25] 3.927s passed
divMinusDenom data()[26] 4.025s passed
divLeastDPos data()[27] 4.041s passed
divLeastDNeg data()[28] 3.853s passed
divGreatestDPos data()[29] 3.839s passed
equivAllRight data()[2] 4.034s passed
divGreatestDNeg data()[30] 3.741s passed
divIncreasingPos data()[31] 3.748s passed
divIncreasingNeg data()[32] 3.702s passed
jdiv_zero data()[33] 3.680s passed
jdivPulloutMinusNum data()[34] 3.691s passed
jdivPulloutMinusDenom data()[35] 3.703s passed
jdiv_uniquePosPos data()[36] 3.704s passed
jdiv_uniquePosNeg data()[37] 3.730s passed
jdiv_uniqueNegPos data()[38] 3.749s passed
jdiv_uniqueNegNeg data()[39] 3.737s passed
irrflConcrete1 data()[3] 3.905s passed
jdivMultDenom1 data()[40] 3.731s passed
jdivMultDenom2 data()[41] 3.654s passed
mod_geZero data()[42] 3.755s passed
mod_lessDenom data()[43] 3.752s passed
jmod_NumPos data()[44] 3.701s passed
jmod_NumNeg data()[45] 3.691s passed
jmod_geZero data()[46] 3.786s passed
jmodNumZero data()[47] 3.738s passed
jmod_pulloutminusNum data()[48] 3.677s passed
jmod_pulloutminusDenom data()[49] 3.710s passed
irrflConcrete2 data()[4] 3.828s passed
jmodUnique1 data()[50] 3.745s passed
jmodUnique2 data()[51] 3.751s passed
intDivRem data()[52] 3.645s passed
jmodjmod data()[53] 3.591s passed
jmodDivisible data()[54] 3.745s passed
jmodDivisibleRep data()[55] 3.709s passed
jdivAddMultDenom data()[56] 3.815s passed
jmodAltZero data()[57] 3.704s passed
jmodAddMultDenomZero data()[58] 3.768s passed
polyDiv_zero data()[59] 3.903s passed
cancel_gtPos data()[5] 3.862s passed
polyMod_ltdivDenom data()[60] 3.767s passed
bsum_empty data()[61] 3.818s passed
bsum_induction_upper data()[62] 3.806s passed
bsum_induction_lower data()[63] 3.789s passed
bsum_num_of_bounds data()[64] 3.753s passed
bsum_num_of_bounds2 data()[65] 3.811s passed
bsum_induction_upper2 data()[66] 3.776s passed
bsum_induction_upper_concrete data()[67] 3.727s passed
bsum_induction_upper_concrete_2 data()[68] 3.838s passed
bsum_induction_upper2_concrete data()[69] 3.677s passed
cancel_gtNeg data()[6] 3.784s passed
bsum_induction_lower_concrete data()[70] 3.782s passed
bsum_induction_lower2 data()[71] 3.778s passed
bsum_induction_lower2_concrete data()[72] 3.814s passed
bsum_positive data()[73] 3.869s passed
bsum_upper_bound data()[74] 3.925s passed
bsum_lower_bound data()[75] 3.902s passed
bsum_positive_lower_bound_element data()[76] 3.814s passed
bsum_sub_same_index data()[77] 3.802s passed
bsum_less_same_index data()[78] 3.907s passed
bsum_equal_except_one_index data()[79] 4.016s passed
moduloIntIsInInt data()[7] 3.779s passed
bsum_num_of_is_max data()[80] 3.979s passed
bsum_num_of_is_max2 data()[81] 4.038s passed
bsum_num_of_is_max3 data()[82] 3.798s passed
bsum_num_of_is_max4 data()[83] 3.816s passed
bsum_num_of_lt_max data()[84] 3.855s passed
bsum_num_of_lt_max2 data()[85] 3.831s passed
bsum_num_of_lt_max3 data()[86] 3.781s passed
bsum_num_of_lt_max4 data()[87] 3.817s passed
bsum_num_of_gt0 data()[88] 3.733s passed
bsum_num_of_gt0_alt data()[89] 3.814s passed
moduloLongIsInLong data()[8] 3.576s passed
bsum_add_concrete data()[90] 3.777s passed
bprod_all_positive data()[91] 3.818s passed
bprod_split data()[92] 3.739s passed
powConcrete0 data()[93] 3.804s passed
powConcrete1 data()[94] 3.771s passed
powSplitFactor data()[95] 3.782s passed
powAdd data()[96] 3.744s passed
powMono data()[97] 3.802s passed
powMonoConcrete data()[98] 3.737s passed
powMonoConcreteRight data()[99] 3.759s passed
moduloShortIsInShort data()[9] 3.666s passed

Standard output

408        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
435        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.96ms 
714        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733        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)

1754       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1756       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1758       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1759       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3163       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8998       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.28s 
9086       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9126       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.3ns 
9139       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9141       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.68ms 
9146       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12159      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
12161      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13224      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13248      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.44ms 
13262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13263      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.41ns 
13265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16185      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
16185      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
17263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
17294      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.89ms 
17299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
17300      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 479.02ns 
17306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20272      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
20273      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
21195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
21202      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
21205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
21205      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.62ns 
21206      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24026      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
24027      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
25025      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
25031      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
25034      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
25034      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.82ns 
25035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27877      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
27878      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
28835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
28892      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.99ms 
28900      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
28900      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.01ns 
28902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31721      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
31722      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
32646      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
32680      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.89ms 
32685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
32685      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 452.32ns 
32687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35513      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
35514      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
36458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
36461      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 799.64ns 
36463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
36463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.91ns 
36464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39121      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
39121      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
40034      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
40037      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 583.13ns 
40040      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
40040      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.12ns 
40041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42745      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
42745      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
43700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
43703      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570.83ns 
43705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
43706      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 431.92ns 
43707      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
46434      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
47516      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
47521      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 706.64ns 
47524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
47524      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.31ns 
47526      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50228      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
50228      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
51168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
51171      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.23ns 
51172      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
51172      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
51173      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54064      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
54065      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
54983      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
55064      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.05ms 
55069      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
55069      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.81ns 
55070      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57789      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
57789      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
58697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
58787      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.02ms 
58792      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
58793      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.72ns 
58795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61604      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
61604      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
62517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
62759      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 232.85ms 
62765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
62766      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 456.42ns 
62767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
65703      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
66635      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
66640      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
66642      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
66642      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.51ns 
66643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69554      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
69554      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
70480      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
70485      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
70487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
70488      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.52ns 
70489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73478      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
73479      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
74473      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
74526      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.67ms 
74529      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
74529      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.72ns 
74530      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77546      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
77546      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
78560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
78578      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.72ms 
78580      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
78580      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.01ns 
78581      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81560      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
81560      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
82531      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
82551      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16ms 
82554      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
82554      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 458.72ns 
82556      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85638      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
85639      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
86598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
86656      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.74ms 
86663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
86663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 459.02ns 
86665      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89646      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
89647      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
90633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
90651      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.67ms 
90653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
90653      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.81ns 
90654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93591      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
93592      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
94586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
94619      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.83ms 
94621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
94621      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.31ns 
94622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97548      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
97549      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
98518      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
98522      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
98523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
98523      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.51ns 
98524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
101493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
102507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
102571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.61ms 
102575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
102575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.12ns 
102577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
105487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
106429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
106499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.44ms 
106502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
106503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.62ns 
106504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
109453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
110467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
110526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.11ms 
110529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
110529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.82ns 
110531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
113544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
114548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
114566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.21ms 
114571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
114571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.51ns 
114572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
117459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
118401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
118421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.65ms 
118423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
118423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.31ns 
118424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
121318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
122247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
122260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.75ms 
122262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
122262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.21ns 
122263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
125076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
125993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
126001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.18ms 
126003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
126003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.81ns 
126004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
128794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
129732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
129747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.07ms 
129754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
129754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.82ns 
129756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
132551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
133445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
133453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
133455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
133455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.41ns 
133456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
136252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
137129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
137133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
137134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
137135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.61ns 
137135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
139925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
140812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
140824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.67ms 
140826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
140826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.51ns 
140827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
143587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
144467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
144527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.79ms 
144530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
144530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.52ns 
144532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
147327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
148213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
148233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.37ms 
148234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
148234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.61ns 
148235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
150995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
151942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
151962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.17ms 
151964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
151964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.71ns 
151965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
154782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
155690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
155710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.14ms 
155713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
155713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.52ns 
155714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
158502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
159428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
159447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.15ms 
159451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
159452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 469.42ns 
159453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
162210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
163134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
163180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.53ms 
163183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
163183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.12ns 
163184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
165923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
166831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
166834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
166836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
166836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.11ns 
166837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
169629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
170583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
170588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
170591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
170591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.91ns 
170592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
173369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
174332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
174341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ms 
174342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
174343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.31ns 
174343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
177119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
178032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
178041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.28ms 
178044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
178044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.32ns 
178045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
180775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
181713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
181733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.29ms 
181734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
181735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.71ns 
181736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
184562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
185511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
185519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ms 
185521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
185521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.81ns 
185521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
188288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
189254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
189257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
189260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
189260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.01ns 
189261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
192002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
192929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
192934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
192935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
192935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.31ns 
192936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
195725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
196641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
196645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
196646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
196646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.61ns 
196647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
199412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
200313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
200389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.25ms 
200390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
200390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.61ns 
200391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
203173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
204045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
204140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.89ms 
204142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
204143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.42ns 
204144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
206923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
207782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
207786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
207787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
207787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.91ns 
207788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
210478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
211336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
211375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.69ms 
211379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
211379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 488.93ns 
211380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
214137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
215087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
215121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.65ms 
215123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
215123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.81ns 
215124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
217912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
218826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
218830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
218835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
218837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.1ms 
218839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
221560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
222473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
222647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 161.71ms 
222650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
222650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.71ns 
222651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
225429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
226341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
226352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.35ms 
226354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
226354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
226355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
229165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
230111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
230120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.86ms 
230121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
230121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
230122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
233040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
234001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
234023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.91ms 
234026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
234026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.81ns 
234027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
236838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
237773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
237789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ms 
237792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
237792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.52ns 
237793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
240666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
241604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
241608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
241610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
241610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
241611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
244464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
245409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
245415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.39ms 
245416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
245416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.41ns 
245417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
248258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
249176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
249203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.62ms 
249204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
249204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.91ns 
249205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
252012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
252937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
252956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.25ms 
252957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
252957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
252958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
255777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
256748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
256767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.62ms 
256772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
256772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.01ns 
256773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
259653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
260542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
260546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
260549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
260549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.51ns 
260550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
263368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
264268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
264273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
264275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
264275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
264275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
267206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
268106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
268112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
268113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
268113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.31ns 
268114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
270883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
271785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
271788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
271789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
271789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
271790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
274631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
275568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
275570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.44ns 
275571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
275572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.01ns 
275572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
278391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
279344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
279349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
279350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
279350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.41ns 
279351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
282206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
283159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
283162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
283164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
283164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
283165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
286023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
286962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
287031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.66ms 
287034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
287034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.81ns 
287035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
289927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
290889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
290956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.71ms 
290958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
290958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.91ns 
290959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
293872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
294816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
294858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.87ms 
294860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
294860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.31ns 
294861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
297698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
298622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
298672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.01ms 
298674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
298674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
298675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
301491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
302437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
302474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.37ms 
302475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
302475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.71ns 
302476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
305373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
306323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
306381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.85ms 
306383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
306383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.91ns 
306384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
309331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
310364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
310397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.71ms 
310398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
310398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.91ns 
310399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
313353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
314347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
314376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.13ms 
314378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
314378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
314379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
317404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
318384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
318414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.57ms 
318416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
318416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.81ns 
318417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
321281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
322189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
322212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.22ms 
322214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
322214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
322215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
325071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
325991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
326029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.21ms 
326030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
326030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
326031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
328929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
329854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
329883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.9ms 
329885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
329885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.41ns 
329886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
332761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
333678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
333714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.22ms 
333716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
333716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.11ns 
333717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
336552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
337466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
337495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.98ms 
337496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
337497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.41ns 
337497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
340328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
341288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
341313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.54ms 
341314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
341314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.41ns 
341315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
344082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
345017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
345045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.56ms 
345046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
345046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
345047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
347882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
348830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
348859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.3ms 
348861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
348861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
348862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
351699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
352628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
352637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.57ms 
352638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
352638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
352639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
355494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
356434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
356454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.43ms 
356455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
356455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
356456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
359231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
360186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
360193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
360195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
360195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.01ns 
360196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
363040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
363993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
363997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
364000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
364000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.61ns 
364001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
366818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
367765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
367768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 848.54ns 
367769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
367769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
367771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
370600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
371539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
371550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ms 
371551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
371552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.61ns 
371552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
374349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
375287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
375294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
375297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
375297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.22ns 
375298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
378124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
379082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
379096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ms 
379098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
379098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
379098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
381892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
382828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
382834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
382835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
382835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
382836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
385685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
386590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
386592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 682.53ns 
386593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
386593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
386594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
389407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
390312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
390318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
390319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
390319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
390320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
393132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
394070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
394073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 688.34ns 
394074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
394074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
394075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
396919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
397840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
397842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 645.03ns 
397844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
397844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
397844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
400667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
401601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
401604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.74ns 
401605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
401605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
401605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
404471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
405391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
405396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
405397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
405397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
405398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
408281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
409236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
409246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.97ms 
409248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
409248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
409248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
412103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
413048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
413052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
413054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
413054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
413055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
415909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
416849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
416857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.22ms 
416859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
416859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
416859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
419704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
420640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
420645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
420646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
420646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
420647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
423489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
424493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
424512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.3ms 
424513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
424513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.21ns 
424514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
427325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
428284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
428289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
428290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
428290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
428291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
431164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
432135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
432138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
432140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
432140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
432141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
434996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
435951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
435955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
435956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
435957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
435958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
438813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
439769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
439790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.48ms 
439791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
439791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
439792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
442670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
443640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
443646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570.63ns 
443648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
443648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
443649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
446526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
447487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
447534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.27ms 
447537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
447537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.91ns 
447538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
450368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
451332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
451336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
451337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
451337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
451338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
454210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
455160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
455188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.96ms 
455192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
455192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.71ns 
455193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
458071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
459004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
459031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.3ms 
459033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
459033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.61ns 
459034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
461870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
462782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
462810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.64ms 
462812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
462812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.91ns 
462813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
465681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
466590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
466593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 805.34ns 
466594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
466594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
466595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
469476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
470409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
470416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
470417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
470418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
470418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
473332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
474299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
474302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
474304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
474304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.91ns 
474306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
477154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
478098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
478101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 912.05ns 
478103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
478103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.91ns 
478104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
480932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
481882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
481885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 913.25ns 
481886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
481886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
481887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
484731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
485689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
485693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
485694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
485694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
485695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
488553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
489492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
489495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
489496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
489496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
489497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
492311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
493259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
493270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ms 
493272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
493272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
493273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
496079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
497031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
497045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.28ms 
497046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
497047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
497047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
499833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
500769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
500781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
500783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
500783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
500784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
503563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
504513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
504530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.73ms 
504531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
504531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
504532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
507290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
508209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
508214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
508215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
508215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
508216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
510975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
511925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
511932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
511933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
511933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
511934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
514725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
515661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
515665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.04ns 
515667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
515667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
515668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
518528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
519486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
519489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
519491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
519491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
519491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
522298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
523254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
523257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
523258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
523259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
523259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
526090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
527023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
527036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.13ms 
527037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
527037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
527038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
529893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
530807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
530812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
530814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
530814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
530815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
533606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
534577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
534585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.14ms 
534586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
534587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
534587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
537444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
538391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
538394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 705.24ns 
538395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
538395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
538396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
541221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
542204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
542206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 681.74ns 
542208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
542208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
542209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
545073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
546023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
546027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
546029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
546029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.81ns 
546030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
548915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
549892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
549895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
549897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
549897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
549897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
552741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
553716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
553719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
553720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
553721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
553721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
556511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
557457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
557461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
557462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
557462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
557463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
560375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
561324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
561331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
561332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
561332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
561333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
564188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
565151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
565154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
565156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
565156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
565156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
568000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
568964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
568978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ms 
568979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
568980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.71ns 
568981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
571768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
572731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
572733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.33ns 
572735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
572735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
572735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
575568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
576539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
576547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.17ms 
576549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
576549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
576549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
579431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
580385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
580388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 970.35ns 
580389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
580389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
580390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
583157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
584125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
584128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
584129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
584129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
584130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
586858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
587780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
587786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
587788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
587788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.11ns 
587789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
590510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
591472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
591475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
591477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
591477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
591478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
594257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
595169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
595173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
595174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
595174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
595175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
597897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
598786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
598790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
598791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
598791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
598792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
601524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
602438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
602443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
602445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
602445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
602446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
605205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
606151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
606170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.3ms 
606172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
606172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
606172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
608929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
609860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
609878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.73ms 
609880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
609880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
609880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
612599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
613512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
613523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.47ms 
613525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
613525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
613526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
616306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
617226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
617239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.04ms 
617241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
617241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
617242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
619991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
620924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
620953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.31ms 
620955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
620955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.21ns 
620955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
623648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
624564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
624595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.18ms 
624596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
624597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
624597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
627384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
628298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
628329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.76ms 
628331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
628331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
628332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
631071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
632018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
632033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.28ms 
632034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
632034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
632035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
634829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
635766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
635802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.21ms 
635803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
635803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.11ns 
635804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
638538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
639481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
639537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.55ms 
639539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
639539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
639540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
642304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
643201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
643249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.99ms 
643251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
643251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.31ns 
643253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
645876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
646759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
646806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.78ms 
646808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
646808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
646809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
649359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
650223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
650267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.29ms 
650268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
650268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
650269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
653002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
653932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
654070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 130.18ms 
654072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
654072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
654072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
656781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
657685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
657693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.09ms 
657694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
657694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
657695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
660374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
661268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
661279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.62ms 
661280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
661280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
661281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
664022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
664926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
664932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
664933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
664933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
664934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
667635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
668517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
668572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.02ms 
668575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
668575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.21ns 
668576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
671287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
672209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
672221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.97ms 
672223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
672223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
672224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
674931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
675838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
675842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
675843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
675843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
675844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
678566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
679488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
679506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
679508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
679508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
679509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
682188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
683116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
683134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.57ms 
683136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
683136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
683136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
685784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
686662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
686731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.59ms 
686732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
686732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
686733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
689343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
690230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
690233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
690235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
690235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
690236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
692870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
693818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
693825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.01ms 
693827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
693827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
693828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
696488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
697357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
697364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
697365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
697365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
697365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
700071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
700966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
700979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.75ms 
700981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
700981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
700982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
703651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
704546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
704623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.86ms 
704625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
704625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
704625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
707300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
708241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
708364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 119.56ms 
708366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
708366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
708366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
711072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
711982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
712005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.11ms 
712007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
712007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
712009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
714817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
715770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
715773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 315.22ns 
715775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
715775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.21ns 
715776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
718538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
719472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
719704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 220.2ms 
719707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
719707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.61ns 
719708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
722512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
723466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
723529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.83ms 
723530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
723530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
723531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
726341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
727295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
727298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 360.42ns 
727299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
727299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
727300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
730140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
731099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
731101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 404.92ns 
731102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
731102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
731103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
733867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
734842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
734844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 410.52ns 
734849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
734850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.91ns 
734851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
737707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
738691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
738693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 530.33ns 
738695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
738695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
738696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
741536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
742458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
742583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 123.3ms 
742588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
742588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.72ns 
742589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
745474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
745474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
746445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
746501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.13ms 
746503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
746503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
746504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
749349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
750315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
750317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ns 
750345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
750383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
750401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
750405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
750411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
750414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
750415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
750417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
750420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
750422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
750424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
750425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
750606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
750608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
750609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
750611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
750612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
750757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
750758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
750762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
750765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
750767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
750769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
751008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
751011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
751012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
751013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
751014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
751017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
751175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
751177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
751179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
751180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
751181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
751182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
751192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
751193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
751194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
751197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
751199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
751201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
751212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
751214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
751215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
751217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
751218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
751219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
751382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
751384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
751386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
751541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
751543     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)'' 
751546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
751548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
751549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
751551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
751552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
751555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
751560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
751562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
751564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
751564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
751565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
751708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
751712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
751714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
751716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
751717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
751718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
751720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
751888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
751890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
751891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
751893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
751894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
751895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
751897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
751899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
752035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
752037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
752227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
752232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
752239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
752241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
752242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
752244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
752246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
752247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
752248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
752249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
752259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
752267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
752390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
752394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
752396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
752398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
752399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
752399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
752400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
752401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
752469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
752477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
752598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
752600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
752602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
752605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
752606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
752607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
752774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
752780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
752783     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)'' 
752786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
752788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
752789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
752789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
752790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
752823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
752832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
752835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
752837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
752978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
752980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
752981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
752982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
752983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
752984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
753124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
753126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
753128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
753130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
753131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
753131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
753132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
753133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
753257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
753260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
753364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
753365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
753366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
753372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
753377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
753383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
753531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
753533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
753534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
753535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
753548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
753657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
757999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
758000     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)'' 
758006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
758007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
758008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
758009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
758010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
758019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
758020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
758021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
758022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
758023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
758132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
758136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
758137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
758138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
758139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
758140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
758141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
758252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
758253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
758254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
758256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
758256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
758257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
758258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
758259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
758350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
758352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
758449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
758454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
758459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
758461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
758462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
758463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
758475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
758576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
758578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
758579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
758580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
758665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
758676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
758677     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)'' 
758680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
758681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
758681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
758682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
758683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
758695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
758697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
758698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
758699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
758700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
758802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
758804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
758805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
758806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
758807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
758919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
758926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
758928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
758929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
758929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
758930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
758931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
759050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
759052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
759053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
759054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
759055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
759056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
759056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
759058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
759059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
759060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
759061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
759062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
759062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
759063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
759064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
759165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
759167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
759174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
759264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
759356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
759357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
759358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
759359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
759360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
759361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
759361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
759361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
759362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
759468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
759475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
759577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
759578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
759579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
759581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
759581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
759582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
759582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
759583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
759589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
759590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
759682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
759688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
759694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
759807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
759808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
759809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
759811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
759811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
759812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
759813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
759814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
759883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
759885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
759886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
759887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
759890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
759897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
759906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
760047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
760198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
760200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
760200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
760201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
760392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
760493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
760494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
764015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
764020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
764021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
764022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
764023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
764151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
764153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
764154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
764155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
764156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
764279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
767829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
771583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
771589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
771590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
771591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
771592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
771728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
771730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
771731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
771733     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)' ...' 
771734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
773067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
773067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.51ns 
773068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
776081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
777010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
777012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
777013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
777019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
777082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
777085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
777087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
777087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
777091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
777093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
777095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
777098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
777099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
777108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
777109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
777110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
777161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
777162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
777162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
777163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
777164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
777232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
777233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
777234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
777235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
777235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
777239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
777239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
777240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
777241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
777241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
777242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
777321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
777321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
777322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
777323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
777324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
777324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
777407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
777407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
777408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
777408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
777409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
777410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
777411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
777411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
777412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
777412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
777413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
777413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
777413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
777414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
777414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
777415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
777415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
777416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
777417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
777419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
777457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
777458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
777508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
777510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
777511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
777512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
777513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
777513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
777558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
777561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
777562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
777564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
777565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
777566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
777566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
777612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
777614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
777617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
777677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
777738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
777738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.41ns 
777739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
780553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
781568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
781603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.7ms