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

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

tests
0

failures
0

ignored
12m45.78s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.626s passed
powPositiveConcrete data()[101] 3.622s passed
powGeq1Concrete data()[102] 3.613s passed
pow2InIntLower data()[103] 3.600s passed
pow2InIntUpper data()[104] 3.598s passed
logSelfConcrete data()[105] 3.591s passed
log1Concrete data()[106] 3.601s passed
logProduct data()[107] 3.603s passed
logTimesBaseConcrete data()[108] 3.601s passed
logProdIdentity data()[109] 3.584s passed
moduloByteIsInByte data()[10] 3.844s passed
logProdIdentityConcrete data()[110] 3.691s passed
logPowIdentity data()[111] 3.715s passed
logPowIdentityConcrete data()[112] 3.729s passed
logPositive data()[113] 3.679s passed
logPositiveConcrete data()[114] 3.721s passed
logMono data()[115] 3.733s passed
logMonoConcrete data()[116] 3.749s passed
powLogLess data()[117] 3.817s passed
powLogMore2 data()[118] 3.810s passed
logLessThanPow data()[119] 3.811s passed
moduloCharIsInChar data()[11] 3.737s passed
logLessThanPowConcrete data()[120] 3.770s passed
logSqueeze data()[121] 3.794s passed
ifthenelse_equals data()[122] 3.727s passed
ifthenelse_equals_1 data()[123] 3.734s passed
ifthenelse_equals_2 data()[124] 3.712s passed
disjointWithSingleton1 data()[125] 3.627s passed
disjointWithSingleton2 data()[126] 3.626s passed
disjointArrayRanges data()[127] 3.679s passed
disjointArrayRangeAllFields1 data()[128] 3.758s passed
disjointArrayRangeAllFields2 data()[129] 3.733s passed
div_unique1 data()[12] 3.785s passed
seqSelfDefinition data()[130] 3.734s passed
seqOutsideValue data()[131] 3.804s passed
castedGetAny data()[132] 3.782s passed
seqGetAlphaCast data()[133] 3.769s passed
getOfSeqSingleton data()[134] 3.723s passed
getOfSeqSingletonConcrete data()[135] 3.778s passed
getOfSeqConcat data()[136] 3.840s passed
getOfSeqSub data()[137] 3.870s passed
getOfSeqReverse data()[138] 3.828s passed
lenOfSeqEmpty data()[139] 3.822s passed
div_unique2 data()[13] 3.795s passed
lenOfSeqSingleton data()[140] 3.791s passed
lenOfSeqConcat data()[141] 3.741s passed
lenOfSeqSub data()[142] 3.707s passed
lenOfSeqReverse data()[143] 3.865s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.841s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.841s passed
getOfSeqSingletonEQ data()[146] 3.807s passed
getOfSeqConcatEQ data()[147] 3.747s passed
getOfSeqSubEQ data()[148] 3.714s passed
getOfSeqReverseEQ data()[149] 3.721s passed
div_exists data()[14] 3.944s passed
lenOfSeqEmptyEQ data()[150] 3.698s passed
lenOfSeqSingletonEQ data()[151] 3.669s passed
lenOfSeqConcatEQ data()[152] 3.636s passed
lenOfSeqSubEQ data()[153] 3.781s passed
lenOfSeqReverseEQ data()[154] 3.704s passed
getOfSeqDefEQ data()[155] 3.745s passed
lenOfSeqDefEQ data()[156] 3.784s passed
seqConcatWithSeqEmpty1 data()[157] 3.739s passed
seqConcatWithSeqEmpty2 data()[158] 3.742s passed
seqReverseOfSeqEmpty data()[159] 3.781s passed
div_one data()[15] 3.793s passed
subSeqComplete data()[160] 3.814s passed
subSeqTailR data()[161] 3.750s passed
subSeqTailL data()[162] 3.759s passed
subSeqTailEQR data()[163] 3.726s passed
subSeqTailEQL data()[164] 3.767s passed
seqDef_split data()[165] 3.783s passed
seqDef_induction_upper data()[166] 3.711s passed
seqDef_induction_upper_concrete data()[167] 3.621s passed
seqDef_induction_lower data()[168] 3.646s passed
seqDef_induction_lower_concrete data()[169] 3.641s passed
jdiv_one data()[16] 3.785s passed
seqDef_split_in_three data()[170] 3.741s passed
seqDef_empty data()[171] 3.740s passed
seqDef_one_summand data()[172] 3.663s passed
seqDef_lower_equals_upper data()[173] 3.632s passed
seqDefOfSeq data()[174] 3.649s passed
seqSelfDefinitionEQ2 data()[175] 3.795s passed
indexOfSeqSingleton data()[176] 3.706s passed
indexOfSeqConcatFirst data()[177] 3.660s passed
indexOfSeqConcatSecond data()[178] 3.693s passed
indexOfSeqSub data()[179] 3.684s passed
div_zero data()[17] 3.884s passed
lenOfArray2seq data()[180] 3.728s passed
getAnyOfArray2seq data()[181] 3.805s passed
getOfArray2seq data()[182] 3.796s passed
getAnyOfNPermInv data()[183] 3.818s passed
seqNPermRange data()[184] 3.861s passed
seqPermTrans data()[185] 3.850s passed
seqPermRefl data()[186] 3.802s passed
seqPermSplit data()[187] 3.824s passed
seqNPermRight data()[188] 3.903s passed
seqPermFromSwap data()[189] 3.895s passed
divResZero1 data()[18] 3.817s passed
seqPermTransAlt0 data()[190] 3.816s passed
seqPermTransAlt1 data()[191] 3.848s passed
seqPermTransAlt2 data()[192] 3.829s passed
seqPermTransAlt3 data()[193] 3.796s passed
seqPermForall data()[194] 3.903s passed
seqPermExists data()[195] 3.819s passed
schiffl_lemma_2 data()[196] 24.377s passed
schiffl_thm_1 data()[197] 4.601s passed
eqSameSeq data()[198] 3.817s passed
divResZero2 data()[19] 3.818s passed
eqTermCut data()[1] 4.572s passed
divResOne1 data()[20] 3.827s passed
divResOne2 data()[21] 3.858s passed
div_cancel1 data()[22] 3.794s passed
div_cancel2 data()[23] 3.839s passed
divAddMultDenom data()[24] 3.865s passed
divMinus data()[25] 3.821s passed
divMinusDenom data()[26] 3.757s passed
divLeastDPos data()[27] 3.772s passed
divLeastDNeg data()[28] 3.806s passed
divGreatestDPos data()[29] 3.792s passed
equivAllRight data()[2] 4.369s passed
divGreatestDNeg data()[30] 3.747s passed
divIncreasingPos data()[31] 3.709s passed
divIncreasingNeg data()[32] 3.695s passed
jdiv_zero data()[33] 3.784s passed
jdivPulloutMinusNum data()[34] 3.730s passed
jdivPulloutMinusDenom data()[35] 3.749s passed
jdiv_uniquePosPos data()[36] 3.695s passed
jdiv_uniquePosNeg data()[37] 3.670s passed
jdiv_uniqueNegPos data()[38] 3.734s passed
jdiv_uniqueNegNeg data()[39] 3.745s passed
irrflConcrete1 data()[3] 4.259s passed
jdivMultDenom1 data()[40] 3.847s passed
jdivMultDenom2 data()[41] 3.710s passed
mod_geZero data()[42] 3.747s passed
mod_lessDenom data()[43] 3.806s passed
jmod_NumPos data()[44] 3.798s passed
jmod_NumNeg data()[45] 3.766s passed
jmod_geZero data()[46] 3.803s passed
jmodNumZero data()[47] 3.833s passed
jmod_pulloutminusNum data()[48] 3.847s passed
jmod_pulloutminusDenom data()[49] 3.807s passed
irrflConcrete2 data()[4] 3.905s passed
jmodUnique1 data()[50] 3.852s passed
jmodUnique2 data()[51] 3.802s passed
intDivRem data()[52] 3.686s passed
jmodjmod data()[53] 3.743s passed
jmodDivisible data()[54] 3.804s passed
jmodDivisibleRep data()[55] 3.736s passed
jdivAddMultDenom data()[56] 3.875s passed
jmodAltZero data()[57] 3.634s passed
jmodAddMultDenomZero data()[58] 3.654s passed
polyDiv_zero data()[59] 3.687s passed
cancel_gtPos data()[5] 4.008s passed
polyMod_ltdivDenom data()[60] 3.618s passed
bsum_empty data()[61] 3.610s passed
bsum_induction_upper data()[62] 3.703s passed
bsum_induction_lower data()[63] 3.686s passed
bsum_num_of_bounds data()[64] 3.660s passed
bsum_num_of_bounds2 data()[65] 3.704s passed
bsum_induction_upper2 data()[66] 3.694s passed
bsum_induction_upper_concrete data()[67] 3.787s passed
bsum_induction_upper_concrete_2 data()[68] 3.719s passed
bsum_induction_upper2_concrete data()[69] 3.712s passed
cancel_gtNeg data()[6] 3.896s passed
bsum_induction_lower_concrete data()[70] 3.797s passed
bsum_induction_lower2 data()[71] 3.756s passed
bsum_induction_lower2_concrete data()[72] 3.708s passed
bsum_positive data()[73] 3.733s passed
bsum_upper_bound data()[74] 3.823s passed
bsum_lower_bound data()[75] 3.762s passed
bsum_positive_lower_bound_element data()[76] 3.816s passed
bsum_sub_same_index data()[77] 3.810s passed
bsum_less_same_index data()[78] 3.852s passed
bsum_equal_except_one_index data()[79] 3.829s passed
moduloIntIsInInt data()[7] 3.954s passed
bsum_num_of_is_max data()[80] 3.708s passed
bsum_num_of_is_max2 data()[81] 3.694s passed
bsum_num_of_is_max3 data()[82] 3.754s passed
bsum_num_of_is_max4 data()[83] 3.741s passed
bsum_num_of_lt_max data()[84] 3.675s passed
bsum_num_of_lt_max2 data()[85] 3.679s passed
bsum_num_of_lt_max3 data()[86] 3.714s passed
bsum_num_of_lt_max4 data()[87] 3.650s passed
bsum_num_of_gt0 data()[88] 3.712s passed
bsum_num_of_gt0_alt data()[89] 3.637s passed
moduloLongIsInLong data()[8] 3.892s passed
bsum_add_concrete data()[90] 3.591s passed
bprod_all_positive data()[91] 3.632s passed
bprod_split data()[92] 3.601s passed
powConcrete0 data()[93] 3.635s passed
powConcrete1 data()[94] 3.727s passed
powSplitFactor data()[95] 3.640s passed
powAdd data()[96] 3.663s passed
powMono data()[97] 3.637s passed
powMonoConcrete data()[98] 3.689s passed
powMonoConcreteRight data()[99] 3.673s passed
moduloShortIsInShort data()[9] 3.743s passed

Standard output

466        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
494        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.75ms 
763        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783        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)

1799       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1811       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1816       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1817       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3368       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10191      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.43s 
10259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10297      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.9ns 
10309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.41ns 
10313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13759      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
13762      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14872      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.06ms 
14884      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14885      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.81ns 
14888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18241      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
18241      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
19226      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19251      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.48ms 
19255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.71ns 
19260      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
22438      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
23498      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
23509      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ms 
23515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23515      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.91ns 
23518      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26429      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
26430      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
27406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
27418      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.41ms 
27426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
27427      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.18ms 
27429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
30377      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
31352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
31424      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.99ms 
31430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
31430      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 875.44ns 
31432      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34328      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
34329      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
35304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
35323      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.91ms 
35329      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
35330      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 486.62ns 
35331      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38279      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
38280      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
39275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
39279      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 646.33ns 
39281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
39282      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.12ns 
39283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42213      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
42213      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
43168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
43171      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 603.13ns 
43174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
43174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.92ns 
43175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45965      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
45966      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
46911      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
46914      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.53ns 
46917      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
46917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 784.54ns 
46919      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49792      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
49792      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
50754      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
50757      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.03ns 
50760      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
50761      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.82ns 
50762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53540      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
53541      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
54491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
54494      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 688.93ns 
54498      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
54498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.22ns 
54500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
57286      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
58227      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
58280      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.5ms 
58282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
58282      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.11ns 
58283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61123      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
61123      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
62043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
62074      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.82ms 
62078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
62079      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.82ns 
62080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64923      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
64924      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
65886      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
66019      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 123.58ms 
66022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
66023      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 447.12ns 
66024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68868      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
68868      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
69806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
69813      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
69816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
69816      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.01ns 
69817      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
72637      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
73595      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
73598      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
73600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
73600      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.01ns 
73601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76462      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
76463      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
77435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
77481      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.51ms 
77485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
77486      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415.12ns 
77487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80330      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
80330      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
81286      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
81299      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
81302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
81302      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.71ns 
81303      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84146      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
84146      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
85105      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
85117      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
85119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
85120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.91ns 
85121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87972      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
87972      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
88930      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
88945      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.34ms 
88948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
88950      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.71ms 
88952      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91828      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
91828      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
92789      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
92802      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.23ms 
92805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
92806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.32ns 
92807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95634      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
95634      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
96571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
96597      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.11ms 
96600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
96600      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.62ns 
96602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99460      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
99460      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
100431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
100436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
100439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
100439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.21ns 
100441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
103302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
104261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
104301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.02ms 
104305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
104305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.42ns 
104307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
107122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
108073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
108123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.85ms 
108126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
108126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.82ns 
108134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
110918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
111847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
111881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.54ms 
111883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
111883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
111884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
114699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
115646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
115653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.25ms 
115655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
115655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.61ns 
115656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
118487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
119441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
119458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.97ms 
119468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
119468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 444.92ns 
119469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
122293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
123245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
123256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
123259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
123259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.61ns 
123260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
126075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
126995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
127003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
127007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
127008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 753.44ns 
127009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
129810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
130707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
130714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
130716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
130716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.31ns 
130717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
133498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
134402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
134409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.44ms 
134410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
134410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.61ns 
134411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
137281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
138189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
138193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
138195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
138195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.81ns 
138196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
141015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
141913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
141924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.55ms 
141925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
141925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.71ns 
141926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
144714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
145634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
145671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.65ms 
145675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
145675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.52ns 
145685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
148450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
149351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
149368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ms 
149370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
149370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.71ns 
149371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
152130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
153022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
153038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.25ms 
153039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
153040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.51ns 
153040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
155850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
156756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
156773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.31ms 
156774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
156774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.11ns 
156775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
159590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
160502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
160517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.46ms 
160519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
160519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.71ns 
160520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
163389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
164328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
164364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.62ms 
164367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
164367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.82ns 
164368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
167191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
168068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
168074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 992.05ns 
168077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
168077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.31ns 
168078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
170896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
171816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
171821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
171822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
171822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.51ns 
171823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
174698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
175620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
175628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.45ms 
175629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
175629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.11ns 
175630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
178494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
179416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
179424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.83ms 
179427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
179427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.52ns 
179428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
182257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
183174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
183191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.27ms 
183193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
183193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.71ns 
183194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
186091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
186987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
186994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms 
186995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
186996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.61ns 
186996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
189840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
190823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
190826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
190829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
190829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.52ns 
190831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
193741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
194669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
194674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
194677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
194677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.12ns 
194678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
197551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
198477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
198481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
198483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
198484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.02ns 
198485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
201352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
202271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
202332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.45ms 
202335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
202336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.72ns 
202337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
205163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
206064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
206135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.23ms 
206137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
206137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.31ns 
206138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
208927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
209818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
209822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
209823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
209823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
209824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
212627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
213531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
213564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.34ms 
213566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
213566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.91ns 
213567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
216430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
217345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
217368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.39ms 
217370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
217370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.31ns 
217371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
220174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
221101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
221104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
221106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
221106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
221107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
223887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
224820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
224979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 147.72ms 
224981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
224981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.41ns 
224982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
227732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
228603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
228613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.61ms 
228615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
228615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.91ns 
228616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
231374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
232261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
232267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 
232268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
232268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.21ns 
232269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
234998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
235938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
235954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.25ms 
235956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
235956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.61ns 
235957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
238651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
239559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
239571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 
239573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
239574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.11ns 
239574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
242276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
243179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
243183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
243184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
243184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
243185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
245959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
246881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
246885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
246886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
246886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
246887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
249637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
250554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
250571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.39ms 
250572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
250572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.91ns 
250573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
253305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
254218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
254231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.21ms 
254233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
254233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
254234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
256998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
257920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
257935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.17ms 
257937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
257937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.92ns 
257940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
260679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
261626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
261629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
261631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
261632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.31ns 
261633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
264472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
265412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
265416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
265417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
265417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
265418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
268199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
269130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
269135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
269136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
269136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
269137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
271882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
272843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
272847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
272849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
272849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.61ns 
272850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
275691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
276642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
276644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 571.43ns 
276646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
276646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
276646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
279463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
280396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
280400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
280401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
280401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
280402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
283206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
284106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
284109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.34ns 
284110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
284110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
284111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
286857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
287799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
287840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.28ms 
287843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
287843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.91ns 
287844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
290695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
291634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
291663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.79ms 
291666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
291667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.41ns 
291668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
294461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
295401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
295427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.76ms 
295428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
295429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.11ns 
295429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
298267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
299209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
299243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.33ms 
299245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
299245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.31ns 
299246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
302087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
303032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
303053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.94ms 
303054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
303054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
303055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
305916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
306861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
306904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.09ms 
306907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
306908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.31ns 
306909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
309775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
310714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
310734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.17ms 
310736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
310736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.51ns 
310737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
313516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
314426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
314442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.69ms 
314443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
314443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.11ns 
314444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
317182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
318118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
318136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.93ms 
318138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
318138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.31ns 
318139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
320931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
321875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
321890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.07ms 
321892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
321892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
321893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
324685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
325612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
325631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.75ms 
325632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
325632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.31ns 
325633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
328359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
329289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
329307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.91ms 
329308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
329308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.11ns 
329309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
332057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
332965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
332985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.18ms 
332986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
332987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.31ns 
332987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
335761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
336681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
336699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.55ms 
336700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
336701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.31ns 
336701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
339399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
340329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
340349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.48ms 
340351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
340352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.11ns 
340353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
343103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
344035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
344061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.6ms 
344063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
344063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.51ns 
344064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
346789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
347682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
347698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms 
347700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
347700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85ns 
347701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
350380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
351282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
351289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
351290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
351290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
351291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
353998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
354908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
354921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.82ms 
354923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
354923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.81ns 
354924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
357619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
358519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
358523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
358524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
358524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
358524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
361232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
362155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
362157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 645.13ns 
362159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
362159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
362159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
364947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
365881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
365884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 826.64ns 
365885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
365885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
365886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
368600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
369517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
369524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
369525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
369525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
369526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
372264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
373181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
373187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
373189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
373189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.51ns 
373190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
375901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
376813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
376824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.68ms 
376825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
376825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
376826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
379579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
380510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
380513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
380515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
380515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
380515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
383260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
384184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
384186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 488.32ns 
384188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
384188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
384189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
386924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
387807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
387812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
387814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
387814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
387814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
390528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
391432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
391435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.73ns 
391437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
391437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.01ns 
391438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
394129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
395045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
395047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 562.03ns 
395049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
395049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
395050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
397749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
398645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
398647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.73ns 
398648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
398648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
398649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
401346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
402241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
402245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
402246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
402246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
402247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
404932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
405828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
405836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.35ms 
405837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
405837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
405838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
408523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
409427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
409436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
409439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
409439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.52ns 
409442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
412136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
413034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
413040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
413042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
413042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
413043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
415726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
416637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
416641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
416642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
416643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
416643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
419309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
420211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
420225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.23ms 
420227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
420227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
420227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
422973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
423911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
423916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 
423917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
423918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
423918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
426703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
427628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
427631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
427632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
427632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
427633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
430418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
431356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
431360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
431361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
431361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
431362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
434119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
435024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
435039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.02ms 
435040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
435040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
435041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
437822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
438755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
438759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 396.62ns 
438762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
438762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
438762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
441544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
442459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
442489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.87ms 
442495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
442495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
442496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
445293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
446238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
446242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
446243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
446243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
446244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
449083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
450042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
450060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.49ms 
450061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
450061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
450062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
452900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
453853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
453870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.24ms 
453871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
453871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
453872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
456713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
457661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
457681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.51ms 
457682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
457682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
457683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
460492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
461447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
461450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 526.54ns 
461454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
461454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.12ns 
461455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
464298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
465240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
465246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
465247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
465247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
465250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
468036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
468969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
468972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
468973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
468973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
468974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
471760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
472704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
472707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 923.85ns 
472708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
472708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
472709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
475477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
476416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
476418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 886.15ns 
476420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
476420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
476421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
479165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
480041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
480045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
480047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
480048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.32ns 
480049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
482749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
483668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
483671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
483673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
483673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
483674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
486458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
487343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
487352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ms 
487353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
487353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
487354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
490171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
491102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
491109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
491110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
491110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
491111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
493935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
494835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
494842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
494844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
494844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
494844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
497660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
498568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
498576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
498578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
498578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.41ns 
498578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
501411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
502376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
502380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
502382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
502382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.21ns 
502383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
505198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
506157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
506162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.66ms 
506163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
506163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
506164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
508966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
509929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
509931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 805.25ns 
509933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
509933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
509934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
512700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
513652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
513655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
513656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
513656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
513657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
516470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
517430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
517433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
517434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
517434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
517435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
520272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
521263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
521273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.75ms 
521275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
521275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.31ns 
521276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
524170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
525140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
525143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
525144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
525145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.61ns 
525145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
527996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
528965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
528971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
528973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
528974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.61ns 
528975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
531834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
532791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
532793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 905.75ns 
532795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
532795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
532795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
535621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
536582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
536584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702.34ns 
536586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
536586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
536587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
539391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
540322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
540325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
540327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
540327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
540328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
543092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
544030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
544033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 948.75ns 
544034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
544034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
544035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
546918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
547894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
547897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
547899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
547899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
547899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
550761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
551736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
551739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
551740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
551740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
551741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
554606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
555575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
555579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
555580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
555580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
555581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
558420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
559384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
559386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 952.05ns 
559388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
559388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
559389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
562183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
563123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
563133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.36ms 
563134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
563134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
563135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
565927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
566845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
566847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540.83ns 
566849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
566849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
566849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
569640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
570562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
570568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.08ms 
570569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
570570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
570571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
573324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
574264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
574267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 911.03ns 
574268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
574268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
574269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
577021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
577932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
577935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 764.14ns 
577936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
577936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
577937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
580640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
581567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
581571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
581573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
581573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
581574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
584434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
585350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
585352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 973.45ns 
585354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
585354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
585355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
588137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
589054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
589057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
589058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
589058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
589059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
591833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
592799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
592802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
592803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
592803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
592804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
595617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
596581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
596585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
596586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
596586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
596587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
599372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
600316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
600324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.19ms 
600326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
600326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
600326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
603139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
604058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
604067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.34ms 
604068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
604068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
604069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
606879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
607841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
607848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
607849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
607849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
607850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
610701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
611655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
611662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
611663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
611663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
611664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
614475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
615400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
615411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.84ms 
615413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
615413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
615414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
618234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
619159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
619171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.88ms 
619172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
619172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.61ns 
619173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
621923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
622886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
622896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.25ms 
622898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
622898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
622899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
625697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
626656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
626663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
626665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
626665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
626665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
629484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
630424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
630446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.73ms 
630448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
630448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
630448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
633192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
634134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
634157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.36ms 
634159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
634159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
634160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
636885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
637758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
637778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.75ms 
637779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
637779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
637780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
640481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
641396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
641424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.64ms 
641426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
641426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.51ns 
641427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
644117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
645043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
645065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.93ms 
645067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
645067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.91ns 
645068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
647842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
648752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
648806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.36ms 
648807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
648807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
648808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
651596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
652541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
652546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
652547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
652547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
652548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
655262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
656204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
656210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.39ms 
656211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
656211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
656212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
658929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
659837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
659841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
659843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
659843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
659844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
662554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
663476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
663490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.21ms 
663492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
663492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
663492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
666343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
667278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
667285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
667286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
667286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
667287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
670043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
670988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
670992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
670993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
670993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
670994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
673759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
674640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
674651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.61ms 
674652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
674652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.31ns 
674653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
677399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
678333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
678345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.75ms 
678346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
678346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
678347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
681128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
682015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
682029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.07ms 
682030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
682030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
682031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
684784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
685753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
685756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 917.15ns 
685758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
685758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
685759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
688626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
689557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
689561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
689562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
689562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
689563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
692395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
693351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
693357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
693358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
693358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
693359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
696235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
697170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
697175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.39ms 
697176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
697176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
697177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
700033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
700989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
701036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.47ms 
701038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
701038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
701039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
703929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
704866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
704886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.35ms 
704888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
704888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
704888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
707752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
708676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
708688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.43ms 
708689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
708690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
708690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
711523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
712510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
712512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 171.71ns 
712515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
712515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.51ns 
712516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
715371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
716326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
716415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.83ms 
716417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
716417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
716418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
719298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
720271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
720310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.01ms 
720312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
720312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
720312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
723173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
724124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
724126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 305.12ns 
724129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
724130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.72ns 
724131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
727008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
727973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
727975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 238.41ns 
727976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
727976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
727977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
730840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
731803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
731805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 234.31ns 
731806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
731806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
731807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
734642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
735598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
735600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 360.92ns 
735601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
735601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
735602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
738444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
739408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
739494     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
739503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.18ms 
739506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
739506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.01ns 
739507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
742335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
743274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
743322     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
743322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.04ms 
743324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
743324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
743325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
746115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
747070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
747071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 
747105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
747143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
747159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
747167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
747183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
747185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
747188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
747190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
747197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
747201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
747203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
747207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
747411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
747412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
747413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
747414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
747415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
747534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
747535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
747536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
747537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
747539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
747540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
747712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
747713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
747715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
747716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
747717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
747718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
747836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
747837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
747840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
747841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
747841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
747843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
747850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
747851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
747853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
747853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
747854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
747855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
747862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
747863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
747864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
747865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
747866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
747867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
747998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
747999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
748001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
748126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
748127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
748128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
748131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
748132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
748133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
748134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
748135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
748139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
748140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
748141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
748142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
748144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
748292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
748296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
748297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
748299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
748300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
748300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
748302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
748423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
748424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
748425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
748427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
748428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
748428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
748429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
748430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
748532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
748534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
748620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
748625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
748629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
748630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
748631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
748632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
748633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
748633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
748634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
748635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
748642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
748647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
748742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
748743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
748744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
748745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
748746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
748746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
748747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
748748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
748800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
748806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
748902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
748903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
748904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
748906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
748907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
748908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
749035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
749040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
749040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
749041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
749043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
749044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
749045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
749045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
749055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
749056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
749057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
749058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
749151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
749152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
749154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
749155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
749155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
749156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
749263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
749264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
749265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
749266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
749267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
749268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
749274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
749275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
749361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
749362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
749440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
749441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
749441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
749446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
749450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
749455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
749581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
749582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
749584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
749585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
749595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
749683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
753650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
753651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
753656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
753658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
753659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
753660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
753661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
753670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
753671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
753672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
753673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
753674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
753778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
753782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
753783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
753784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
753785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
753786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
753787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
753892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
753894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
753895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
753896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
753897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
753897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
753898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
753899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
753986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
753987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
754076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
754082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
754087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
754089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
754091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
754092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
754104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
754199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
754201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
754202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
754203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
754284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
754294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
754295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
754296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
754298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
754299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
754299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
754300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
754312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
754313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
754314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
754315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
754316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
754414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
754415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
754416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
754417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
754418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
754517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
754523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
754524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
754525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
754526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
754526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
754527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
754640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
754641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
754642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
754643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
754645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
754645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
754646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
754647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
754648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
754649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
754650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
754651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
754651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
754652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
754653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
754751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
754752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
754759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
754846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
754937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
754938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
754939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
754940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
754941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
754941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
754942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
754942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
754943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
755039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
755046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
755146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
755147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
755148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
755149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
755150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
755150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
755151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
755151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
755157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
755158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
755247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
755258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
755265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
755383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
755384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
755385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
755386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
755387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
755387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
755387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
755388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
755451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
755452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
755453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
755453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
755454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
755460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
755466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
755597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
755745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
755746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
755746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
755747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
755931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
756028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
756029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
759320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
759325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
759326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
759327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
759328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
759455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
759456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
759457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
759458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
759459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
759572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
762864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
766288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
766292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
766293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
766294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
766295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
766484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
766484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
766485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
766487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
766487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
767701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
767701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.11ns 
767702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
770635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
771626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
771628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
771628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
771636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
771646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
771649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
771651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
771653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
771658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
771659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
771663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
771664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
771666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
771676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
771677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
771678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
771728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
771729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
771730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
771730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
771731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
771795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
771796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
771796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
771797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
771798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
771802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
771802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
771803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
771803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
771804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
771805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
771885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
771886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
771886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
771887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
771888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
771889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
771974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
771975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
771975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
771976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
771976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
771977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
771977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
771978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
771979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
771979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
771979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
771980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
771980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
771981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
771981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
771981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
771982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
771982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
771983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
771986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
772022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
772023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
772079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
772080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
772081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
772082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
772083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
772084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
772131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
772134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
772135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
772135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
772136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
772137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
772138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
772184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
772186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
772190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
772244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
772301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
772301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
772302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
775125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
776099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
776117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.58ms