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

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

tests
0

failures
0

ignored
12m25.32s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.641s passed
powPositiveConcrete data()[101] 3.717s passed
powGeq1Concrete data()[102] 3.528s passed
pow2InIntLower data()[103] 3.516s passed
pow2InIntUpper data()[104] 3.663s passed
logSelfConcrete data()[105] 3.576s passed
log1Concrete data()[106] 3.568s passed
logProduct data()[107] 3.572s passed
logTimesBaseConcrete data()[108] 3.462s passed
logProdIdentity data()[109] 3.541s passed
moduloByteIsInByte data()[10] 3.574s passed
logProdIdentityConcrete data()[110] 3.778s passed
logPowIdentity data()[111] 3.740s passed
logPowIdentityConcrete data()[112] 3.672s passed
logPositive data()[113] 3.705s passed
logPositiveConcrete data()[114] 3.552s passed
logMono data()[115] 3.498s passed
logMonoConcrete data()[116] 3.470s passed
powLogLess data()[117] 3.769s passed
powLogMore2 data()[118] 3.726s passed
logLessThanPow data()[119] 3.544s passed
moduloCharIsInChar data()[11] 3.989s passed
logLessThanPowConcrete data()[120] 3.582s passed
logSqueeze data()[121] 3.685s passed
ifthenelse_equals data()[122] 3.631s passed
ifthenelse_equals_1 data()[123] 3.691s passed
ifthenelse_equals_2 data()[124] 3.662s passed
disjointWithSingleton1 data()[125] 3.732s passed
disjointWithSingleton2 data()[126] 3.631s passed
disjointArrayRanges data()[127] 3.667s passed
disjointArrayRangeAllFields1 data()[128] 3.582s passed
disjointArrayRangeAllFields2 data()[129] 3.613s passed
div_unique1 data()[12] 3.725s passed
seqSelfDefinition data()[130] 3.586s passed
seqOutsideValue data()[131] 3.651s passed
castedGetAny data()[132] 3.651s passed
seqGetAlphaCast data()[133] 3.684s passed
getOfSeqSingleton data()[134] 3.553s passed
getOfSeqSingletonConcrete data()[135] 3.652s passed
getOfSeqConcat data()[136] 3.642s passed
getOfSeqSub data()[137] 3.599s passed
getOfSeqReverse data()[138] 3.458s passed
lenOfSeqEmpty data()[139] 3.657s passed
div_unique2 data()[13] 3.750s passed
lenOfSeqSingleton data()[140] 3.569s passed
lenOfSeqConcat data()[141] 3.596s passed
lenOfSeqSub data()[142] 3.789s passed
lenOfSeqReverse data()[143] 3.623s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.725s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.712s passed
getOfSeqSingletonEQ data()[146] 3.805s passed
getOfSeqConcatEQ data()[147] 3.504s passed
getOfSeqSubEQ data()[148] 3.553s passed
getOfSeqReverseEQ data()[149] 3.594s passed
div_exists data()[14] 3.780s passed
lenOfSeqEmptyEQ data()[150] 3.765s passed
lenOfSeqSingletonEQ data()[151] 3.605s passed
lenOfSeqConcatEQ data()[152] 3.608s passed
lenOfSeqSubEQ data()[153] 3.573s passed
lenOfSeqReverseEQ data()[154] 3.745s passed
getOfSeqDefEQ data()[155] 3.683s passed
lenOfSeqDefEQ data()[156] 3.719s passed
seqConcatWithSeqEmpty1 data()[157] 3.561s passed
seqConcatWithSeqEmpty2 data()[158] 3.691s passed
seqReverseOfSeqEmpty data()[159] 3.521s passed
div_one data()[15] 3.667s passed
subSeqComplete data()[160] 3.618s passed
subSeqTailR data()[161] 3.504s passed
subSeqTailL data()[162] 3.655s passed
subSeqTailEQR data()[163] 3.570s passed
subSeqTailEQL data()[164] 3.541s passed
seqDef_split data()[165] 3.704s passed
seqDef_induction_upper data()[166] 3.722s passed
seqDef_induction_upper_concrete data()[167] 3.683s passed
seqDef_induction_lower data()[168] 3.718s passed
seqDef_induction_lower_concrete data()[169] 3.669s passed
jdiv_one data()[16] 3.911s passed
seqDef_split_in_three data()[170] 3.607s passed
seqDef_empty data()[171] 3.479s passed
seqDef_one_summand data()[172] 3.457s passed
seqDef_lower_equals_upper data()[173] 3.587s passed
seqDefOfSeq data()[174] 3.535s passed
seqSelfDefinitionEQ2 data()[175] 3.510s passed
indexOfSeqSingleton data()[176] 3.442s passed
indexOfSeqConcatFirst data()[177] 3.602s passed
indexOfSeqConcatSecond data()[178] 3.471s passed
indexOfSeqSub data()[179] 3.597s passed
div_zero data()[17] 3.616s passed
lenOfArray2seq data()[180] 3.550s passed
getAnyOfArray2seq data()[181] 3.784s passed
getOfArray2seq data()[182] 3.669s passed
getAnyOfNPermInv data()[183] 3.525s passed
seqNPermRange data()[184] 3.545s passed
seqPermTrans data()[185] 3.688s passed
seqPermRefl data()[186] 3.651s passed
seqPermSplit data()[187] 3.661s passed
seqNPermRight data()[188] 3.596s passed
seqPermFromSwap data()[189] 3.477s passed
divResZero1 data()[18] 3.612s passed
seqPermTransAlt0 data()[190] 3.421s passed
seqPermTransAlt1 data()[191] 3.578s passed
seqPermTransAlt2 data()[192] 3.467s passed
seqPermTransAlt3 data()[193] 3.555s passed
seqPermForall data()[194] 3.631s passed
seqPermExists data()[195] 3.788s passed
schiffl_lemma_2 data()[196] 24.825s passed
schiffl_thm_1 data()[197] 4.225s passed
eqSameSeq data()[198] 3.517s passed
divResZero2 data()[19] 3.595s passed
eqTermCut data()[1] 4.357s passed
divResOne1 data()[20] 3.561s passed
divResOne2 data()[21] 3.801s passed
div_cancel1 data()[22] 3.770s passed
div_cancel2 data()[23] 3.788s passed
divAddMultDenom data()[24] 3.822s passed
divMinus data()[25] 3.704s passed
divMinusDenom data()[26] 3.779s passed
divLeastDPos data()[27] 3.651s passed
divLeastDNeg data()[28] 3.635s passed
divGreatestDPos data()[29] 3.766s passed
equivAllRight data()[2] 4.248s passed
divGreatestDNeg data()[30] 3.785s passed
divIncreasingPos data()[31] 3.606s passed
divIncreasingNeg data()[32] 3.559s passed
jdiv_zero data()[33] 3.607s passed
jdivPulloutMinusNum data()[34] 3.777s passed
jdivPulloutMinusDenom data()[35] 3.694s passed
jdiv_uniquePosPos data()[36] 3.831s passed
jdiv_uniquePosNeg data()[37] 3.709s passed
jdiv_uniqueNegPos data()[38] 3.834s passed
jdiv_uniqueNegNeg data()[39] 3.757s passed
irrflConcrete1 data()[3] 4.046s passed
jdivMultDenom1 data()[40] 3.653s passed
jdivMultDenom2 data()[41] 3.626s passed
mod_geZero data()[42] 3.606s passed
mod_lessDenom data()[43] 3.581s passed
jmod_NumPos data()[44] 3.549s passed
jmod_NumNeg data()[45] 3.547s passed
jmod_geZero data()[46] 3.562s passed
jmodNumZero data()[47] 3.591s passed
jmod_pulloutminusNum data()[48] 3.516s passed
jmod_pulloutminusDenom data()[49] 3.558s passed
irrflConcrete2 data()[4] 3.961s passed
jmodUnique1 data()[50] 3.649s passed
jmodUnique2 data()[51] 3.857s passed
intDivRem data()[52] 3.735s passed
jmodjmod data()[53] 3.529s passed
jmodDivisible data()[54] 3.573s passed
jmodDivisibleRep data()[55] 3.712s passed
jdivAddMultDenom data()[56] 3.789s passed
jmodAltZero data()[57] 3.633s passed
jmodAddMultDenomZero data()[58] 3.467s passed
polyDiv_zero data()[59] 3.700s passed
cancel_gtPos data()[5] 3.995s passed
polyMod_ltdivDenom data()[60] 3.701s passed
bsum_empty data()[61] 3.696s passed
bsum_induction_upper data()[62] 3.683s passed
bsum_induction_lower data()[63] 3.756s passed
bsum_num_of_bounds data()[64] 3.524s passed
bsum_num_of_bounds2 data()[65] 3.571s passed
bsum_induction_upper2 data()[66] 3.522s passed
bsum_induction_upper_concrete data()[67] 3.816s passed
bsum_induction_upper_concrete_2 data()[68] 3.720s passed
bsum_induction_upper2_concrete data()[69] 3.679s passed
cancel_gtNeg data()[6] 3.723s passed
bsum_induction_lower_concrete data()[70] 3.505s passed
bsum_induction_lower2 data()[71] 3.556s passed
bsum_induction_lower2_concrete data()[72] 3.692s passed
bsum_positive data()[73] 3.672s passed
bsum_upper_bound data()[74] 3.799s passed
bsum_lower_bound data()[75] 3.528s passed
bsum_positive_lower_bound_element data()[76] 3.649s passed
bsum_sub_same_index data()[77] 3.635s passed
bsum_less_same_index data()[78] 3.674s passed
bsum_equal_except_one_index data()[79] 3.736s passed
moduloIntIsInInt data()[7] 3.646s passed
bsum_num_of_is_max data()[80] 3.745s passed
bsum_num_of_is_max2 data()[81] 3.556s passed
bsum_num_of_is_max3 data()[82] 3.657s passed
bsum_num_of_is_max4 data()[83] 3.742s passed
bsum_num_of_lt_max data()[84] 3.590s passed
bsum_num_of_lt_max2 data()[85] 3.573s passed
bsum_num_of_lt_max3 data()[86] 3.711s passed
bsum_num_of_lt_max4 data()[87] 3.668s passed
bsum_num_of_gt0 data()[88] 3.599s passed
bsum_num_of_gt0_alt data()[89] 3.617s passed
moduloLongIsInLong data()[8] 3.589s passed
bsum_add_concrete data()[90] 3.602s passed
bprod_all_positive data()[91] 3.716s passed
bprod_split data()[92] 3.619s passed
powConcrete0 data()[93] 3.534s passed
powConcrete1 data()[94] 3.736s passed
powSplitFactor data()[95] 3.674s passed
powAdd data()[96] 3.819s passed
powMono data()[97] 3.779s passed
powMonoConcrete data()[98] 3.704s passed
powMonoConcreteRight data()[99] 3.639s passed
moduloShortIsInShort data()[9] 3.662s passed

Standard output

370        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
396        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.62ms 
636        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651        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)

1705       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1708       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1712       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1712       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3350       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9160       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.52s 
9256       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9300       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.9ns 
9317       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9317       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 543.21ns 
9324       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
12452      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13625      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13663      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.72ms 
13676      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13677      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.9ns 
13680      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16812      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
16813      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
17898      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
17923      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.26ms 
17926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
17926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.8ns 
17929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20960      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
20961      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
21962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
21969      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
21972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
21973      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.7ns 
21974      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
24915      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
25926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
25932      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
25935      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
25935      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.2ns 
25941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28888      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
28888      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
29886      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
29927      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.32ms 
29932      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
29932      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 503ns 
29934      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
32780      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
33632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
33650      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.08ms 
33655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
33655      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.8ns 
33657      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36407      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
36408      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
37295      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
37299      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 891.91ns 
37300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
37301      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.2ns 
37302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40012      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
40012      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
40885      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
40888      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 613.11ns 
40890      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
40890      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.4ns 
40891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43607      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
43608      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
44548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
44550      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.11ns 
44552      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
44552      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.7ns 
44553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47225      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
47226      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
48120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
48123      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 666.61ns 
48129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
48129      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 684.41ns 
48132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51111      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
51111      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
52112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
52115      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.01ns 
52118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
52119      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 429ns 
52120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54891      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
54892      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
55800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
55839      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.16ms 
55844      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
55846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.04ms 
55847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58581      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
58582      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
59525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
59590      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.88ms 
59594      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
59595      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 753.41ns 
59598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62314      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
62315      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
63195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
63372      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 167.46ms 
63375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
63376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.4ns 
63377      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66115      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
66115      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
67034      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
67040      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
67041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
67042      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.7ns 
67043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
69916      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
70943      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
70951      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
70954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
70954      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403ns 
70955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73637      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
73637      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
74525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
74567      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.73ms 
74571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
74571      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.5ns 
74572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77277      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
77278      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
78164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
78179      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ms 
78182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
78183      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.81ns 
78184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
80881      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
81762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
81775      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.92ms 
81777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
81777      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.7ns 
81778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84447      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
84447      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
85321      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
85335      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.26ms 
85338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
85339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.4ns 
85340      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88164      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
88165      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
89114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
89135      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.98ms 
89142      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
89144      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.93ms 
89145      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92001      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
92001      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
92888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
92910      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.49ms 
92911      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
92912      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.9ns 
92913      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95785      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
95785      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
96693      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
96697      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
96700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
96701      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.8ns 
96702      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99499      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
99501      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
100472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
100520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.92ms 
100523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
100523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.1ns 
100525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
103278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
104173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
104223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.92ms 
104226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
104228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.47ms 
104230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
107016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
107962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
108002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.48ms 
108009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
108012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.78ms 
108013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
110770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
111648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
111655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
111656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
111656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
111657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
114352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
115270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
115289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.87ms 
115292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
115292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.1ns 
115293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
118123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
119039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
119056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ms 
119063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
119063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.2ns 
119064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
121888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
122837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
122844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
122849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
122849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.1ns 
122850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
125606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
126446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
126453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
126455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
126456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.8ns 
126457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
129130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
130003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
130012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
130014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
130015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377ns 
130016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
132708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
133615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
133619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
133620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
133620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
133621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
136438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
137384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
137396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.27ms 
137397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
137397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
137400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
140134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
141055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
141089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.57ms 
141099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
141099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.81ns 
141107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
143992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
144904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
144921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 
144923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
144924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326ns 
144925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
147677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
148579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
148630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.98ms 
148632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
148632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.7ns 
148633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
151521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
152448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
152464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.63ms 
152466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
152466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.6ns 
152467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
155295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
156194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
156221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.09ms 
156222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
156222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns 
156223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
158948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
159841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
159874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.85ms 
159876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
159876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
159877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
162572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
163493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
163499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
163503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
163504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.4ns 
163505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
166217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
167101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
167105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
167108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
167108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.9ns 
167109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
169791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
170680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
170687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
170688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
170689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
170689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
173338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
174228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
174236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.84ms 
174237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
174238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.7ns 
174238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
176920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
177767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
177784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.06ms 
177785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
177785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
177786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
180472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
181338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
181345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.33ms 
181347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
181347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
181348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
184064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
184933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
184936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
184938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
184939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.4ns 
184940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
187545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
188448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
188452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
188454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
188454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.7ns 
188455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
191116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
192005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
192010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
192012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
192012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.4ns 
192014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
194698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
195589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
195658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.56ms 
195663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
195663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.4ns 
195664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
198467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
199436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
199517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.34ms 
199519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
199519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
199520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
202332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
203248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
203252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
203254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
203254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.5ns 
203255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
205905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
206749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
206780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.81ms 
206783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
206784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 480.11ns 
206785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
209428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
210330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
210353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.57ms 
210356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
210356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.9ns 
210357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
213148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
214061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
214066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
214068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
214068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
214069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
216846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
217738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
217854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 101.82ms 
217857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
217857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.1ns 
217858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
220607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
221480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
221488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.42ms 
221490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
221490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
221490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
224074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
224949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
224955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
224957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
224957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
224958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
227743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
228640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
228655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.56ms 
228656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
228656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
228657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
231436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
232343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
232356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
232358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
232358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.3ns 
232359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
235127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
236045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
236051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
236054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
236054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.9ns 
236056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
238838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
239730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
239735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
239738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
239739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.4ns 
239740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
242612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
243477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
243492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.79ms 
243494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
243494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
243495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
246125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
247001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
247014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.26ms 
247019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
247020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 826.41ns 
247021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
249727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
250576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
250589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.79ms 
250590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
250590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
250591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
253197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
254106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
254110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
254112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
254112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.5ns 
254113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
256954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
257922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
257926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
257927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
257928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
257928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
260724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
261641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
261646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
261648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
261648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
261648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
264478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
265322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
265325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
265326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
265327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
265327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
267984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
268829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
268831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 554.11ns 
268832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
268832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
268833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
271504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
272382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
272386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
272387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
272387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.7ns 
272388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
275139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
276075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
276078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 749.31ns 
276081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
276081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.7ns 
276082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
278775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
279696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
279751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.23ms 
279753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
279762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.02ms 
279764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
282601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
283519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
283549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.29ms 
283552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
283552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.9ns 
283553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
286198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
287055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
287078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.97ms 
287080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
287080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
287081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
289789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
290691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
290727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.59ms 
290729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
290730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 697.31ns 
290731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
293489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
294339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
294362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.68ms 
294363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
294363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
294364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
297114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
297994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
298036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.04ms 
298038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
298038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
298039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
300857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
301752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
301773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.83ms 
301774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
301774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
301775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
304573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
305502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
305517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.11ms 
305518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
305519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
305519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
308194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
309056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
309073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.84ms 
309074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
309074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
309075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
311793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
312715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
312730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.38ms 
312732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
312732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.6ns 
312733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
315550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
316451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
316472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.11ms 
316474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
316474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378ns 
316475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
319131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
320044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
320062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.74ms 
320064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
320064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
320065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
322752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
323618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
323635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.41ms 
323637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
323637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
323638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
326435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
327327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
327345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.67ms 
327348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
327348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
327349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
330104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
330995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
331013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms 
331016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
331016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.4ns 
331017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
333739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
334597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
334613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.68ms 
334615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
334615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
334616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
337305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
338212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
338230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.92ms 
338232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
338232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
338232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
340918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
341823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
341832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
341834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
341834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
341835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
344608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
345537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
345549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
345550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
345550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.1ns 
345551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
348288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
349163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
349167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
349169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
349170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.2ns 
349171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
351870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
352699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
352701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 555.51ns 
352705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
352705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.8ns 
352707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
355508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
356436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
356439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.81ns 
356441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
356441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.8ns 
356442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
359193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
360107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
360113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
360114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
360114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
360115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
362974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
363927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
363932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
363934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
363934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
363935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
366773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
367700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
367711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
367712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
367712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
367713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
370499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
371412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
371415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
371416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
371416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
371417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
374157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
375052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
375054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 447.6ns 
375055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
375055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
375056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
377782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
378690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
378695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
378696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
378696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
378697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
381486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
382411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
382413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 478.61ns 
382414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
382414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
382414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
385094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
385939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
385941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 418.5ns 
385942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
385942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
385943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
388553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
389454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
389456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 537.3ns 
389458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
389459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.9ns 
389460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
392211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
393115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
393119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
393121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
393122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.1ns 
393123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
395820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
396687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
396695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.46ms 
396696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
396696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
396697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
399381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
400260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
400263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
400264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
400264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
400265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
402974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
403830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
403836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
403837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
403837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
403838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
406449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
407293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
407298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
407299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
407299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
407300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
409934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
410821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
410838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
410839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
410839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
410840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
413690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
414613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
414617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
414618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
414618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
414619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
417428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
418353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
418357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
418358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
418358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
418359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
421076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
422024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
422028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
422029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
422029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
422030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
424827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
425720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
425733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
425734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
425739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.08ms 
425739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
428404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
429280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
429285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 306.5ns 
429287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
429287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
429288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
431877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
432754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
432783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.99ms 
432784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
432784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
432785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
435393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
436250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
436253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
436255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
436255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
436256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
439077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
440004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
440022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.85ms 
440023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
440023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
440024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
442828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
443730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
443748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.47ms 
443750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
443750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.6ns 
443751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
446404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
447272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
447292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.51ms 
447294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
447294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
447295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
449966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
450872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
450874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 539.71ns 
450876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
450876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
450876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
453639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
454554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
454559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
454560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
454561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
454561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
457267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
458186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
458190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
458192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
458192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.3ns 
458193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
460946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
461878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
461882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 845.71ns 
461884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
461884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
461885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
464681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
465541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
465543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 726.81ns 
465547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
465547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
465548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
468390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
469272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
469277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
469279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
469279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.5ns 
469280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
472001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
472905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
472908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
472910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
472910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
472911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
475673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
476567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
476576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ms 
476577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
476577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
476578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
479260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
480150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
480157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
480158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
480159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
480159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
482876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
483764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
483771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
483772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
483772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
483773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
486404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
487349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
487357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
487358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
487358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
487359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
490097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
491003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
491007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
491009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
491009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.3ns 
491010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
493768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
494653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
494658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
494659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
494659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
494660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
497483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
498340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
498342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 923.71ns 
498344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
498344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
498345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
500951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
501891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
501895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
501897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
501897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.8ns 
501898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
504631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
505545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
505547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 802.81ns 
505549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
505550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334ns 
505551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
508285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
509179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
509189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ms 
509191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
509191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.9ns 
509192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
511901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
512786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
512789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
512790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
512790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
512791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
515380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
516240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
516246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
516247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
516247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
516248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
518973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
519901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
519903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 841.91ns 
519905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
519905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
519906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
522579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
523470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
523472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 641.01ns 
523473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
523473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
523474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
526166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
527065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
527068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
527069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
527070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.1ns 
527070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
529925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
530850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
530856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
530859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
530860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342ns 
530861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
533579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
534478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
534481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
534482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
534482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
534483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
537279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
538202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
538205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
538206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
538206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
538207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
540939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
541912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
541917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
541918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
541918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
541919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
544765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
545719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
545722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 786.81ns 
545723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
545723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
545724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
548345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
549216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
549226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.26ms 
549227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
549227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
549228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
551874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
552777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
552779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 536.21ns 
552780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
552780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
552781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
555460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
556367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
556373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.96ms 
556375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
556375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
556375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
559175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
560135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
560138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
560140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
560140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
560140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
562839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
563741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
563743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 769.91ns 
563744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
563744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
563745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
566444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
567348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
567351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
567353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
567353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
567353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
569985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
570921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
570924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.01ns 
570926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
570926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.5ns 
570927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
573711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
574666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
574670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
574671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
574671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
574672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
577395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
578349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
578353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
578354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
578354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
578355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
581135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
582066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
582071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
582073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
582073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
582074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
584761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
585624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
585632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.96ms 
585633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
585633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
585634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
588384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
589314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
589323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.67ms 
589325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
589325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
589326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
591957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
592838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
592845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
592846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
592846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
592847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
595558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
596456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
596463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
596464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
596464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
596465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
599105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
599956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
599967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.36ms 
599968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
599968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
599969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
602713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
603606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
603621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
603623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
603624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 660.21ns 
603625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
606344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
607181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
607191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ms 
607193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
607193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
607193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
609834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
610725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
610732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.31ms 
610734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
610734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
610735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
613506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
614414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
614436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.75ms 
614438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
614438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
614439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
617170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
618133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
618158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.76ms 
618160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
618160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
618160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
620884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
621818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
621841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.89ms 
621843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
621843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
621844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
624625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
625538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
625560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.64ms 
625562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
625562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
625563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
628269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
629207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
629229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.57ms 
629230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
629230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
629232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
631930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
632783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
632836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.09ms 
632838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
632838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
632838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
635446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
636310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
636314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
636316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
636316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
636317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
638888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
639767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
639772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.36ms 
639774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
639774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
639774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
642432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
643356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
643359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
643361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
643361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
643362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
646001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
646881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
646895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.64ms 
646896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
646896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
646897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
649525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
650397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
650404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
650405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
650405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
650406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
652997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
653844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
653847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
653848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
653848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
653849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
656501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
657430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
657448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.97ms 
657450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
657450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.3ns 
657451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
660028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
660906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
660919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
660920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
660920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
660921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
663616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
664502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
664516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.22ms 
664517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
664517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
664518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
667152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
668062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
668066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
668068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
668068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
668069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
670837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
671847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
671850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
671852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
671852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
671852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
674623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
675514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
675520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
675521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
675521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
675522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
678157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
679039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
679044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
679045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
679046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
679046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
681678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
682542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
682589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.06ms 
682590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
682590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
682591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
685315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
686257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
686277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.95ms 
686279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
686279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
686279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
689001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
689916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
689928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ms 
689930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
689930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
689931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
692723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
693587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
693589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 206.41ns 
693590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
693590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
693592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
696219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
697096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
697185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.28ms 
697187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
697187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
697188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
699750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
700623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
700662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.58ms 
700664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
700664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
700665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
703234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
704081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
704083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 352.7ns 
704085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
704085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
704085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
706764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
707659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
707661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 215.5ns 
707662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
707662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
707663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
710242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
711127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
711129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 214.9ns 
711130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
711130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
711131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
713829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
714682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
714684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 332.8ns 
714685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
714685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
714686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
717328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
718196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
718301     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
718313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.55ms 
718317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
718317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.4ns 
718318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
721125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
722051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
722102     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
722103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.9ms 
722105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
722105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
722106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
724885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
725838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
725840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 
725876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
725910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
725925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
725931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
725943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
725946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
725948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
725949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
725954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
725955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
725957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
725959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
726212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
726213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
726215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
726215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
726217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
726387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
726389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
726392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
726393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
726395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
726398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
726623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
726626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
726627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
726628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
726629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
726632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
726810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
726812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
726814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
726815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
726816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
726817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
726828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
726829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
726832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
726832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
726835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
726836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
726846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
726848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
726849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
726850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
726850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
726852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
727003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
727005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
727006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
727139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
727140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
727141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
727144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
727145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
727146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
727148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
727149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
727153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
727154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
727156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
727157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
727158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
727272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
727276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
727278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
727279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
727281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
727282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
727287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
727421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
727422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
727423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
727425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
727426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
727427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
727428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
727429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
727544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
727546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
727648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
727652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
727659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
727660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
727663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
727665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
727665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
727666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
727667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
727667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
727676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
727681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
727791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
727792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
727794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
727796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
727797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
727797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
727798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
727799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
727853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
727861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
727962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
727963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
727965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
727967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
727968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
727969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
728110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
728121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
728124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
728126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
728127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
728128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
728129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
728130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
728140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
728146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
728147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
728148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
728252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
728253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
728254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
728255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
728256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
728257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
728368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
728369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
728371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
728373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
728374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
728375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
728375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
728376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
728470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
728471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
728557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
728558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
728559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
728563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
728568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
728573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
728717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
728718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
728719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
728721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
728732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
728826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
732956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
732957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
732962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
732964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
732964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
732965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
732966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
732975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
732975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
732977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
732978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
732979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
733081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
733084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
733085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
733086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
733087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
733087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
733088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
733191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
733192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
733193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
733194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
733195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
733196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
733197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
733197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
733285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
733286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
733377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
733382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
733386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
733387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
733388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
733389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
733402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
733499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
733500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
733501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
733502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
733584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
733595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
733595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
733597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
733598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
733600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
733601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
733601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
733613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
733614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
733615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
733616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
733617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
733713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
733714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
733715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
733716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
733718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
733822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
733827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
733828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
733829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
733829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
733830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
733831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
733939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
733940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
733941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
733943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
733943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
733944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
733944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
733945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
733946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
733946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
733947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
733948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
733948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
733949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
733950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
734046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
734047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
734054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
734141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
734230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
734231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
734232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
734233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
734234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
734235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
734235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
734235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
734236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
734330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
734337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
734437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
734438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
734439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
734440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
734440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
734441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
734441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
734442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
734447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
734448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
734533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
734539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
734545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
734655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
734656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
734657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
734658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
734658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
734659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
734659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
734659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
734724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
734725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
734726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
734726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
734727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
734734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
734740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
734954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
735047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
735048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
735049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
735050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
735230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
735328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
735329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
738608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
738613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
738614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
738614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
738615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
738736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
738736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
738737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
738738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
738739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
738852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
742141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
745486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
745491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
745492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
745493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
745494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
745621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
745621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
745622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
745625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
745626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
746930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
746930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.7ns 
746931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
749633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
750466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
750467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
750468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
750475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
750484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
750486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
750488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
750490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
750495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
750495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
750499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
750499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
750502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
750511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
750512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
750513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
750565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
750566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
750566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
750567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
750567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
750633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
750634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
750634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
750635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
750636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
750640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
750640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
750641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
750641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
750642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
750643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
750716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
750717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
750717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
750718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
750719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
750720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
750798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
750798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
750863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
750863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
750864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
750864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
750865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
750865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
750866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
750866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
750867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
750867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
750867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
750867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
750868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
750868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
750868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
750869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
750870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
750872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
750905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
750906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
750952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
750953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
750953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
750955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
750955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
750956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
750998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
751001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
751001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
751002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
751003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
751004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
751005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
751048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
751051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
751054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
751104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
751154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
751154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
751155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
753736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
754648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
754670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.62ms