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

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

tests
0

failures
0

ignored
12m52.06s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.711s passed
powPositiveConcrete data()[101] 3.646s passed
powGeq1Concrete data()[102] 3.678s passed
pow2InIntLower data()[103] 3.715s passed
pow2InIntUpper data()[104] 3.683s passed
logSelfConcrete data()[105] 3.710s passed
log1Concrete data()[106] 3.677s passed
logProduct data()[107] 3.723s passed
logTimesBaseConcrete data()[108] 3.703s passed
logProdIdentity data()[109] 3.678s passed
moduloByteIsInByte data()[10] 3.861s passed
logProdIdentityConcrete data()[110] 3.861s passed
logPowIdentity data()[111] 3.927s passed
logPowIdentityConcrete data()[112] 3.883s passed
logPositive data()[113] 3.737s passed
logPositiveConcrete data()[114] 3.709s passed
logMono data()[115] 3.714s passed
logMonoConcrete data()[116] 3.682s passed
powLogLess data()[117] 3.760s passed
powLogMore2 data()[118] 3.734s passed
logLessThanPow data()[119] 3.755s passed
moduloCharIsInChar data()[11] 3.758s passed
logLessThanPowConcrete data()[120] 3.650s passed
logSqueeze data()[121] 3.651s passed
ifthenelse_equals data()[122] 3.652s passed
ifthenelse_equals_1 data()[123] 3.696s passed
ifthenelse_equals_2 data()[124] 3.630s passed
disjointWithSingleton1 data()[125] 3.786s passed
disjointWithSingleton2 data()[126] 3.727s passed
disjointArrayRanges data()[127] 3.729s passed
disjointArrayRangeAllFields1 data()[128] 3.751s passed
disjointArrayRangeAllFields2 data()[129] 3.857s passed
div_unique1 data()[12] 3.805s passed
seqSelfDefinition data()[130] 3.780s passed
seqOutsideValue data()[131] 3.724s passed
castedGetAny data()[132] 3.714s passed
seqGetAlphaCast data()[133] 3.729s passed
getOfSeqSingleton data()[134] 3.689s passed
getOfSeqSingletonConcrete data()[135] 3.795s passed
getOfSeqConcat data()[136] 3.678s passed
getOfSeqSub data()[137] 3.766s passed
getOfSeqReverse data()[138] 3.747s passed
lenOfSeqEmpty data()[139] 3.709s passed
div_unique2 data()[13] 4.090s passed
lenOfSeqSingleton data()[140] 3.744s passed
lenOfSeqConcat data()[141] 3.729s passed
lenOfSeqSub data()[142] 3.725s passed
lenOfSeqReverse data()[143] 3.756s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.742s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.795s passed
getOfSeqSingletonEQ data()[146] 3.753s passed
getOfSeqConcatEQ data()[147] 3.784s passed
getOfSeqSubEQ data()[148] 3.795s passed
getOfSeqReverseEQ data()[149] 3.815s passed
div_exists data()[14] 4.516s passed
lenOfSeqEmptyEQ data()[150] 3.746s passed
lenOfSeqSingletonEQ data()[151] 3.770s passed
lenOfSeqConcatEQ data()[152] 3.676s passed
lenOfSeqSubEQ data()[153] 3.687s passed
lenOfSeqReverseEQ data()[154] 3.722s passed
getOfSeqDefEQ data()[155] 3.669s passed
lenOfSeqDefEQ data()[156] 3.688s passed
seqConcatWithSeqEmpty1 data()[157] 3.757s passed
seqConcatWithSeqEmpty2 data()[158] 3.764s passed
seqReverseOfSeqEmpty data()[159] 3.693s passed
div_one data()[15] 3.924s passed
subSeqComplete data()[160] 3.718s passed
subSeqTailR data()[161] 3.811s passed
subSeqTailL data()[162] 3.746s passed
subSeqTailEQR data()[163] 3.916s passed
subSeqTailEQL data()[164] 3.771s passed
seqDef_split data()[165] 4.090s passed
seqDef_induction_upper data()[166] 3.731s passed
seqDef_induction_upper_concrete data()[167] 3.804s passed
seqDef_induction_lower data()[168] 3.948s passed
seqDef_induction_lower_concrete data()[169] 4.072s passed
jdiv_one data()[16] 3.778s passed
seqDef_split_in_three data()[170] 3.914s passed
seqDef_empty data()[171] 3.724s passed
seqDef_one_summand data()[172] 3.703s passed
seqDef_lower_equals_upper data()[173] 3.771s passed
seqDefOfSeq data()[174] 3.750s passed
seqSelfDefinitionEQ2 data()[175] 3.750s passed
indexOfSeqSingleton data()[176] 3.697s passed
indexOfSeqConcatFirst data()[177] 3.756s passed
indexOfSeqConcatSecond data()[178] 3.721s passed
indexOfSeqSub data()[179] 3.713s passed
div_zero data()[17] 3.815s passed
lenOfArray2seq data()[180] 3.720s passed
getAnyOfArray2seq data()[181] 3.700s passed
getOfArray2seq data()[182] 3.722s passed
getAnyOfNPermInv data()[183] 3.693s passed
seqNPermRange data()[184] 3.821s passed
seqPermTrans data()[185] 3.872s passed
seqPermRefl data()[186] 3.847s passed
seqPermSplit data()[187] 3.666s passed
seqNPermRight data()[188] 4.302s passed
seqPermFromSwap data()[189] 3.896s passed
divResZero1 data()[18] 3.893s passed
seqPermTransAlt0 data()[190] 3.740s passed
seqPermTransAlt1 data()[191] 3.709s passed
seqPermTransAlt2 data()[192] 3.787s passed
seqPermTransAlt3 data()[193] 3.693s passed
seqPermForall data()[194] 3.849s passed
seqPermExists data()[195] 3.816s passed
schiffl_lemma_2 data()[196] 25.888s passed
schiffl_thm_1 data()[197] 4.643s passed
eqSameSeq data()[198] 4.018s passed
divResZero2 data()[19] 3.847s passed
eqTermCut data()[1] 4.750s passed
divResOne1 data()[20] 3.775s passed
divResOne2 data()[21] 3.833s passed
div_cancel1 data()[22] 3.828s passed
div_cancel2 data()[23] 3.774s passed
divAddMultDenom data()[24] 3.823s passed
divMinus data()[25] 3.887s passed
divMinusDenom data()[26] 3.833s passed
divLeastDPos data()[27] 3.737s passed
divLeastDNeg data()[28] 3.925s passed
divGreatestDPos data()[29] 3.787s passed
equivAllRight data()[2] 4.241s passed
divGreatestDNeg data()[30] 3.781s passed
divIncreasingPos data()[31] 3.807s passed
divIncreasingNeg data()[32] 3.782s passed
jdiv_zero data()[33] 3.799s passed
jdivPulloutMinusNum data()[34] 3.792s passed
jdivPulloutMinusDenom data()[35] 3.768s passed
jdiv_uniquePosPos data()[36] 3.761s passed
jdiv_uniquePosNeg data()[37] 3.665s passed
jdiv_uniqueNegPos data()[38] 3.794s passed
jdiv_uniqueNegNeg data()[39] 3.700s passed
irrflConcrete1 data()[3] 4.230s passed
jdivMultDenom1 data()[40] 3.737s passed
jdivMultDenom2 data()[41] 3.710s passed
mod_geZero data()[42] 3.745s passed
mod_lessDenom data()[43] 3.667s passed
jmod_NumPos data()[44] 3.757s passed
jmod_NumNeg data()[45] 3.750s passed
jmod_geZero data()[46] 3.737s passed
jmodNumZero data()[47] 3.747s passed
jmod_pulloutminusNum data()[48] 3.758s passed
jmod_pulloutminusDenom data()[49] 3.784s passed
irrflConcrete2 data()[4] 3.963s passed
jmodUnique1 data()[50] 3.910s passed
jmodUnique2 data()[51] 3.920s passed
intDivRem data()[52] 3.711s passed
jmodjmod data()[53] 3.696s passed
jmodDivisible data()[54] 3.766s passed
jmodDivisibleRep data()[55] 3.718s passed
jdivAddMultDenom data()[56] 3.918s passed
jmodAltZero data()[57] 3.691s passed
jmodAddMultDenomZero data()[58] 3.802s passed
polyDiv_zero data()[59] 3.776s passed
cancel_gtPos data()[5] 3.963s passed
polyMod_ltdivDenom data()[60] 3.874s passed
bsum_empty data()[61] 3.751s passed
bsum_induction_upper data()[62] 4.045s passed
bsum_induction_lower data()[63] 3.766s passed
bsum_num_of_bounds data()[64] 3.739s passed
bsum_num_of_bounds2 data()[65] 3.691s passed
bsum_induction_upper2 data()[66] 3.721s passed
bsum_induction_upper_concrete data()[67] 3.661s passed
bsum_induction_upper_concrete_2 data()[68] 3.706s passed
bsum_induction_upper2_concrete data()[69] 3.691s passed
cancel_gtNeg data()[6] 3.987s passed
bsum_induction_lower_concrete data()[70] 3.669s passed
bsum_induction_lower2 data()[71] 3.639s passed
bsum_induction_lower2_concrete data()[72] 3.637s passed
bsum_positive data()[73] 3.730s passed
bsum_upper_bound data()[74] 3.808s passed
bsum_lower_bound data()[75] 3.744s passed
bsum_positive_lower_bound_element data()[76] 3.820s passed
bsum_sub_same_index data()[77] 3.739s passed
bsum_less_same_index data()[78] 3.766s passed
bsum_equal_except_one_index data()[79] 3.795s passed
moduloIntIsInInt data()[7] 3.896s passed
bsum_num_of_is_max data()[80] 3.767s passed
bsum_num_of_is_max2 data()[81] 3.770s passed
bsum_num_of_is_max3 data()[82] 3.758s passed
bsum_num_of_is_max4 data()[83] 3.769s passed
bsum_num_of_lt_max data()[84] 3.825s passed
bsum_num_of_lt_max2 data()[85] 3.716s passed
bsum_num_of_lt_max3 data()[86] 3.711s passed
bsum_num_of_lt_max4 data()[87] 3.749s passed
bsum_num_of_gt0 data()[88] 3.771s passed
bsum_num_of_gt0_alt data()[89] 3.702s passed
moduloLongIsInLong data()[8] 3.892s passed
bsum_add_concrete data()[90] 3.701s passed
bprod_all_positive data()[91] 3.732s passed
bprod_split data()[92] 3.699s passed
powConcrete0 data()[93] 3.687s passed
powConcrete1 data()[94] 3.700s passed
powSplitFactor data()[95] 3.687s passed
powAdd data()[96] 3.723s passed
powMono data()[97] 3.693s passed
powMonoConcrete data()[98] 3.699s passed
powMonoConcreteRight data()[99] 3.660s passed
moduloShortIsInShort data()[9] 3.741s passed

Standard output

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

2039       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2041       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2042       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2043       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3312       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11016      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.98s 
11096      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11141      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.2ns 
11156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11156      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.5ns 
11160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
14809      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15865      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15896      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.03ms 
15911      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15912      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 711.63ns 
15914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
19138      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20150      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms 
20154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20154      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.52ns 
20156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23336      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
23337      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24372      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24380      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
24383      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24384      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.81ns 
24387      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27326      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
27327      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
28331      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
28345      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.64ms 
28350      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
28350      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 560.72ns 
28352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31329      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
31330      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
32262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
32311      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.85ms 
32313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
32313      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.41ns 
32314      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35341      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
35341      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
36275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
36298      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.16ms 
36300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
36300      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.81ns 
36302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39251      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
39252      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
40190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
40194      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 819.13ns 
40196      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
40196      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.31ns 
40197      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43118      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
43118      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
44082      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
44086      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 613.42ns 
44088      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
44089      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.61ns 
44090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46907      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
46908      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
47825      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
47828      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 598.42ns 
47830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
47831      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.01ns 
47833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50729      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
50729      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
51686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
51689      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 622.42ns 
51691      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
51691      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
51692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54523      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
54523      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
55444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
55447      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.02ns 
55449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
55449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140ns 
55450      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58262      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
58262      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
59169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
59252      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.84ms 
59254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
59254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.41ns 
59255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62292      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
62292      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
63287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
63341      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.44ms 
63345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
63345      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.62ns 
63347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66481      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
66481      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
67550      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
67855      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 294.68ms 
67862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
67863      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 605.12ns 
67864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70861      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
70861      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
71777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
71784      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
71787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
71787      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.92ns 
71788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74624      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
74625      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
75556      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
75561      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
75565      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
75565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 504.32ns 
75567      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78407      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
78408      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
79326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
79378      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.12ms 
79381      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
79381      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.21ns 
79383      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82272      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
82273      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
83246      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
83271      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.81ms 
83273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
83273      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.91ns 
83275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86133      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
86133      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
87101      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
87119      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.76ms 
87120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
87120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.9ns 
87121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89934      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
89934      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
90865      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
90893      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.12ms 
90896      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
90897      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 517.31ns 
90898      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93771      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
93772      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
94705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
94725      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.59ms 
94728      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
94728      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.91ns 
94729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97603      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
97603      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
98520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
98554      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.17ms 
98556      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
98557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.61ns 
98558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
101432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
102325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
102328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
102329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
102329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.9ns 
102330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
105148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
106085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
106150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.21ms 
106154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
106156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.72ms 
106157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
109048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
109959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
110037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.85ms 
110041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
110041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.31ns 
110043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
112896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
113807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
113872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.12ms 
113874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
113875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.61ns 
113876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
116676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
117598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
117609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.79ms 
117611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
117612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.91ns 
117613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
120510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
121517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
121534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.79ms 
121535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
121535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
121537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
124370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
125306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
125321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.03ms 
125323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
125323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
125324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
128202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
129092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
129102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ms 
129104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
129104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
129105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
131964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
132900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
132909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ms 
132911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
132912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.81ns 
132913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
135723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
136679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
136691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ms 
136693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
136694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.41ns 
136695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
139582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
140486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
140491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
140492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
140492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
140493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
143362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
144269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
144282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ms 
144284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
144284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
144285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
147075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
147979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
148049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.15ms 
148052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
148052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.01ns 
148053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
150864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
151783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
151811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.73ms 
151814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
151814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.31ns 
151815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
154547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
155451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
155477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.27ms 
155478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
155478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.8ns 
155479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
158346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
159245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
159270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.4ms 
159274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
159274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.91ns 
159275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
162058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
162947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
162970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.46ms 
162972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
162972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.61ns 
162973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
165758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
166650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
166707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.41ms 
166708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
166709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
166709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
169485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
170414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
170417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
170420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
170420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
170420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
173255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
174157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
174163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.41ms 
174164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
174164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
174165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
176938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
177820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
177829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.41ms 
177831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
177831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
177833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
180614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
181575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
181586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ms 
181588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
181588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
181588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
184403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
185299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
185335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.05ms 
185338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
185338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.41ns 
185339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
188151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
189059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
189071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.92ms 
189079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
189080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.11ns 
189081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
191879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
192819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
192823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
192825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
192826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.21ns 
192827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
195668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
196577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
196582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
196583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
196583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
196584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
199448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
200360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
200366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
200367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
200367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
200368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
203237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
204158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
204275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.64ms 
204278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
204278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.41ns 
204279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
207139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
208074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
208195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.9ms 
208197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
208197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.31ns 
208198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
211003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
211902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
211906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
211908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
211908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
211909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
214641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
215544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
215602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.35ms 
215604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
215604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.41ns 
215605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
218414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
219324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
219368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.87ms 
219369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
219369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
219370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
222182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
223083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
223086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
223088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
223088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
223089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
225893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
226789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
227004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 203.26ms 
227007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
227007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.71ns 
227008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
229754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
230680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
230695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.03ms 
230697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
230697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
230698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
233574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
234484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
234497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.59ms 
234499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
234499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
234500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
237293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
238250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
238274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.91ms 
238279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
238279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
238279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
241187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
242133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
242150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.84ms 
242152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
242152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
242153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
244962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
245898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
245902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
245903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
245903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
245904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
248972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
249940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
249946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
249947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
249947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
249948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
252795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
253681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
253712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.77ms 
253714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
253714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
253715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
256520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
257426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
257451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.96ms 
257453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
257453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
257454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
260235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
261120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
261142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.01ms 
261143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
261143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
261144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
263962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
264859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
264863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
264865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
264865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
264865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
267608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
268520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
268525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
268526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
268526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
268527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
271318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
272223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
272230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.81ms 
272231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
272232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
272232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
275008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
275918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
275921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
275923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
275923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
275923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
278698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
279588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
279590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 772.13ns 
279592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
279592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
279592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
282342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
283225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
283230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
283231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
283231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
283232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
285991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
286864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
286866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
286868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
286868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
286869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
289619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
290514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
290596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.67ms 
290599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
290600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.91ns 
290601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
293459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
294356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
294404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.67ms 
294406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
294406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
294407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
297204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
298105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
298148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.67ms 
298150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
298150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
298151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
300997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
301905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
301968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.71ms 
301969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
301969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
301970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
304751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
305664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
305707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.79ms 
305708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
305709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
305710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
308503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
309397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
309473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.77ms 
309475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
309475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.31ns 
309476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
312300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
313229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
313267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.56ms 
313270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
313270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
313271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
316100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
317004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
317035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.4ms 
317039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
317039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.21ns 
317040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
319839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
320771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
320807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.73ms 
320808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
320809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
320809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
323627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
324540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
324565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.55ms 
324567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
324567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
324568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
327377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
328296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
328335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.87ms 
328337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
328337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
328339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
331200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
332125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
332160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.37ms 
332161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
332162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
332162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
334939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
335839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
335876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.81ms 
335879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
335879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.01ns 
335881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
338659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
339558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
339589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.85ms 
339590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
339590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.1ns 
339591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
342397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
343311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
343338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.09ms 
343339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
343339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
343340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
346173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
347072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
347108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.22ms 
347110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
347110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
347111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
349898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
350775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
350809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.82ms 
350812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
350812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.81ns 
350813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
353615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
354503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
354511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.81ms 
354513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
354513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
354513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
357344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
358220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
358243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.91ms 
358245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
358245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
358246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
361019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
361937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
361942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
361944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
361944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.61ns 
361946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
364736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
365626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
365629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.62ns 
365630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
365630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
365631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
368423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
369327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
369330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 839.93ns 
369331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
369331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.9ns 
369332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
372094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
373002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
373015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.88ms 
373020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
373020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.01ns 
373021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
375840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
376732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
376740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
376741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
376741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
376742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
379550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
380417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
380432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.86ms 
380434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
380434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
380435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
383207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
384127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
384131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
384132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
384132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
384133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
386913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
387789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
387792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
387793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
387793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
387794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
390586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
391495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
391502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 
391504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
391504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
391504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
394275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
395145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
395148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.82ns 
395149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
395150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.2ns 
395151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
397920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
398824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
398827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 779.93ns 
398828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
398828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
398829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
401614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
402539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
402542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 745.93ns 
402543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
402543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
402545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
405313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
406219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
406224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
406225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
406225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
406226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
409001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
409922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
409934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.96ms 
409935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
409935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
409936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
412736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
413607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
413611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
413612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
413612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
413613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
416437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
417325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
417335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.38ms 
417336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
417337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.51ns 
417337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
420117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
421031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
421037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
421038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
421039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
421039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
423813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
424694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
424715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.97ms 
424717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
424717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
424718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
427595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
428572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
428576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
428577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
428577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
428578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
431541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
432499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
432503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
432504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
432505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
432505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
435488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
436382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
436386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
436387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
436387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
436388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
439211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
440102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
440123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.2ms 
440125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
440125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
440125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
442932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
443827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
443832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 880.53ns 
443834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
443834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.9ns 
443835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
446604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
447496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
447547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.02ms 
447548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
447548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
447549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
450309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
451225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
451229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
451230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
451230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
451231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
454038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
454962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
454989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.83ms 
454990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
454990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
454991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
457800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
458698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
458724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.38ms 
458725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
458725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
458726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
461532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
462448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
462478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.59ms 
462479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
462479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
462480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
465249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
466125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
466128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.23ns 
466130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
466130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.91ns 
466131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
468896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
469771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
469779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.43ms 
469780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
469780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
469781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
472545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
473428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
473431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
473433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
473433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
473433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
476233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
477124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
477127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
477129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
477129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
477130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
479872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
480756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
480759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
480760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
480760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
480761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
483621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
484539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
484544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
484545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
484545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
484546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
487378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
488268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
488271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
488280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
488281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.71ns 
488282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
491087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
491988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
492001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.64ms 
492003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
492003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
492003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
494802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
495736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
495752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.2ms 
495753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
495753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
495754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
498639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
499594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
499609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.64ms 
499610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
499610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.11ns 
499611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
502447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
503368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
503389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ms 
503391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
503391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.91ns 
503392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
506195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
507108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
507113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.98ms 
507115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
507115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
507116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
509878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
510817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
510828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.64ms 
510829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
510829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
510830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
513635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
514554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
514556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 693.93ns 
514557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
514557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
514558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
517325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
518242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
518246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
518247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
518247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
518248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
521124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
522037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
522040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 948.34ns 
522041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
522041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
522042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
524786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
525703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
525718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ms 
525719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
525719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
525720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
528570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
529480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
529485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
529486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
529486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
529487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
532303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
533224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
533232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.99ms 
533233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
533233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
533234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
536037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
536938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
536940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.54ns 
536942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
536942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
536942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
539732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
540682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
540684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 732.33ns 
540685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
540685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
540686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
543507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
544409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
544414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
544415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
544415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.21ns 
544416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
547230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
548135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
548138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
548139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
548139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
548140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
550964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
551891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
551894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
551895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
551895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
551896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
554669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
555632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
555636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
555637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
555637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
555638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
558511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
559425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
559431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
559433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
559433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
559434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
562259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
563182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
563185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
563186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
563186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
563187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
566010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
566953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
566968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.65ms 
566969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
566969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
566970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
569753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
570759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
570763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
570764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
570765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
570765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
573648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
574570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
574578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
574580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
574580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
574581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
577414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
578321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
578324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
578326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
578326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.21ns 
578327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
581146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
582092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
582095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 982.93ns 
582096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
582096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
582097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
584856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
585764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
585770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 
585772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
585772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
585773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
588555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
589453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
589457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
589458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
589458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
589459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
592274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
593175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
593179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
593180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
593180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
593181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
595934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
596844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
596848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
596850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
596850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
596850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
599602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
600530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
600537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
600538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
600538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.1ns 
600539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
603347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
604274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
604293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.49ms 
604294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
604294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
604295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
607132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
608037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
608057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.23ms 
608058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
608058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
608059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
610838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
611737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
611750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.31ms 
611754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
611754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
611755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
614545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
615457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
615470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.15ms 
615471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
615471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
615472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
618321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
619247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
619281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.6ms 
619283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
619283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
619284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
622080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
622993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
623027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.29ms 
623028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
623029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
623029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
625957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
626911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
626943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.08ms 
626945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
626945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
626946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
629740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
630695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
630714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.05ms 
630715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
630716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
630716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
633832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
634761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
634804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.06ms 
634806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
634806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
634807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
637573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
638476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
638535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.21ms 
638537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
638537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
638538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
641365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
642286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
642339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.39ms 
642341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
642341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
642342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
645191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
646231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
646287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.79ms 
646289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
646289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
646290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
649360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
650303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
650360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.54ms 
650362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
650362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
650363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
653201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
654117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
654273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 150.41ms 
654275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
654275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
654276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
657079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
657989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
657997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.94ms 
657999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
657999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
658000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
660748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
661691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
661700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.51ms 
661701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
661701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
661703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
664533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
665465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
665472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
665473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
665473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
665474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
668276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
669199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
669222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.1ms 
669223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
669223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
669224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
672014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
672956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
672972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
672973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
672973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
672974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
675757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
676665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
676669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
676670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
676670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
676671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
679485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
680401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
680424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.94ms 
680425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
680426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
680426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
683202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
684124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
684145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.28ms 
684146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
684146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
684147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
686911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
687834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
687859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.58ms 
687860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
687860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
687861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
690646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
691575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
691579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
691580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
691580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
691581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
694366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
695274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
695278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
695279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
695279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
695280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
698060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
698991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
699001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.81ms 
699002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
699002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
699003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
701781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
702683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
702693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.09ms 
702694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
702696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
702697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
705489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
706413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
706514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.86ms 
706515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
706515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
706516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
709360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
710325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
710377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.72ms 
710388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
710388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.01ns 
710389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
713279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
714206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
714233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.5ms 
714235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
714235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
714236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
716972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
717896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
717899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 413.21ns 
717900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
717900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
717901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
720890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
721887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
722201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 302.09ms 
722204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
722204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.6ns 
722205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
725110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
726032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
726097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.32ms 
726099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
726099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
726099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
728928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
729835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
729838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 380.21ns 
729839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
729839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
729840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
732627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
733544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
733546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 429.11ns 
733548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
733548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
733549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
736367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
737327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
737330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 427.21ns 
737336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
737336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
737337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
740121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
741025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
741028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 725.12ns 
741029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
741029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
741030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
743789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
744742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
744855     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
744876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 129.96ms 
744879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
744879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.41ns 
744881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
747713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
748634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
748693     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
748694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.65ms 
748695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
748695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
748697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
751599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
751599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
752524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
752526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 
752559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
752597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
752615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
752620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
752626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
752629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
752630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
752632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
752635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
752637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
752639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
752640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
752834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
752836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
752837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
752838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
752839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
752960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
752961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
752962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
752964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
752965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
752966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
753151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
753153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
753154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
753154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
753155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
753156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
753297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
753299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
753301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
753302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
753303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
753304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
753312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
753313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
753314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
753316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
753317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
753318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
753326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
753327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
753328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
753329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
753329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
753330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
753498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
753499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
753500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
753650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
753652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
753655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
753656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
753657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
753658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
753659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
753659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
753664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
753665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
753667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
753668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
753668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
753801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
753805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
753807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
753808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
753809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
753809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
753810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
753951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
753952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
753954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
753959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
753960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
753961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
753961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
753963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
754075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
754077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
754179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
754184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
754189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
754190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
754191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
754193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
754193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
754194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
754195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
754196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
754205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
754210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
754369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
754370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
754372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
754374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
754374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
754375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
754375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
754376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
754438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
754446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
754550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
754551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
754553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
754555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
754555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
754558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
754707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
754714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
754716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
754718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
754719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
754720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
754722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
754722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
754732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
754734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
754735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
754736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
754842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
754844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
754844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
754845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
754846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
754847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
754957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
754959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
754960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
754967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
754967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
754968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
754969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
754970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
755109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
755111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
755193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
755193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
755194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
755199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
755203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
755209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
755355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
755357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
755357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
755358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
755369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
755469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
759684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
759686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
759692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
759693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
759694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
759694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
759695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
759704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
759705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
759706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
759707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
759708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
759814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
759818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
759820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
759820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
759821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
759822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
759823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
759935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
759936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
759937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
759939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
759939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
759940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
759941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
759942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
760033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
760034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
760131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
760136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
760141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
760142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
760143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
760144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
760157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
760264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
760265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
760266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
760268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
760359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
760371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
760372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
760374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
760375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
760375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
760376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
760377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
760397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
760402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
760404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
760405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
760406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
760520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
760523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
760524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
760525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
760526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
760634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
760640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
760641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
760641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
760642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
760643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
760643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
760752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
760753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
760754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
760755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
760756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
760757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
760757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
760758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
760759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
760760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
760763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
760764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
760764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
760765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
760766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
760874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
760876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
760882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
760970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
761068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
761071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
761072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
761073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
761074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
761074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
761074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
761075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
761076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
761182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
761189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
761296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
761297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
761298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
761299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
761299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
761300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
761300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
761301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
761308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
761309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
761449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
761456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
761462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
761572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
761573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
761574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
761575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
761575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
761576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
761576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
761577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
761638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
761639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
761640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
761641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
761641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
761647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
761658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
761814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
761918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
761919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
761920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
761921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
762115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
762218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
762219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
765861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
765867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
765868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
765869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
765869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
766005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
766007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
766008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
766009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
766009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
766135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
769556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
773128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
773133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
773134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
773134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
773135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
773264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
773265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
773266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
773267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
773269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
774583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
774583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
774584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
777480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
777480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
778421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
778423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
778423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
778430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
778443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
778446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
778448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
778448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
778453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
778455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
778458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
778462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
778463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
778473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
778475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
778476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
778530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
778531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
778532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
778532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
778533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
778616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
778617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
778618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
778619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
778620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
778624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
778624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
778626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
778627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
778628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
778628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
778717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
778718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
778718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
778719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
778720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
778721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
778823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
778824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
778825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
778825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
778826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
778827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
778828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
778828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
778829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
778830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
778830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
778833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
778833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
778834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
778835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
778835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
778836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
778837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
778839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
778841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
778894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
778896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
778960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
778963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
778964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
778966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
778966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
778967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
779027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
779030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
779031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
779034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
779036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
779036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
779038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
779097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
779100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
779104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
779165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
779226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
779226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
779227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
782228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
783204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
783243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.11ms