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

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

tests
0

failures
0

ignored
11m25.21s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.330s passed
powPositiveConcrete data()[101] 3.321s passed
powGeq1Concrete data()[102] 3.327s passed
pow2InIntLower data()[103] 3.341s passed
pow2InIntUpper data()[104] 3.324s passed
logSelfConcrete data()[105] 3.327s passed
log1Concrete data()[106] 3.327s passed
logProduct data()[107] 3.359s passed
logTimesBaseConcrete data()[108] 3.329s passed
logProdIdentity data()[109] 3.344s passed
moduloByteIsInByte data()[10] 3.402s passed
logProdIdentityConcrete data()[110] 3.327s passed
logPowIdentity data()[111] 3.315s passed
logPowIdentityConcrete data()[112] 3.342s passed
logPositive data()[113] 3.330s passed
logPositiveConcrete data()[114] 3.321s passed
logMono data()[115] 3.335s passed
logMonoConcrete data()[116] 3.335s passed
powLogLess data()[117] 3.329s passed
powLogMore2 data()[118] 3.323s passed
logLessThanPow data()[119] 3.358s passed
moduloCharIsInChar data()[11] 3.433s passed
logLessThanPowConcrete data()[120] 3.324s passed
logSqueeze data()[121] 3.325s passed
ifthenelse_equals data()[122] 3.341s passed
ifthenelse_equals_1 data()[123] 3.324s passed
ifthenelse_equals_2 data()[124] 3.328s passed
disjointWithSingleton1 data()[125] 3.347s passed
disjointWithSingleton2 data()[126] 3.324s passed
disjointArrayRanges data()[127] 3.326s passed
disjointArrayRangeAllFields1 data()[128] 3.350s passed
disjointArrayRangeAllFields2 data()[129] 3.334s passed
div_unique1 data()[12] 3.545s passed
seqSelfDefinition data()[130] 3.348s passed
seqOutsideValue data()[131] 3.364s passed
castedGetAny data()[132] 3.331s passed
seqGetAlphaCast data()[133] 3.365s passed
getOfSeqSingleton data()[134] 3.320s passed
getOfSeqSingletonConcrete data()[135] 3.346s passed
getOfSeqConcat data()[136] 3.343s passed
getOfSeqSub data()[137] 3.360s passed
getOfSeqReverse data()[138] 3.337s passed
lenOfSeqEmpty data()[139] 3.351s passed
div_unique2 data()[13] 3.548s passed
lenOfSeqSingleton data()[140] 3.335s passed
lenOfSeqConcat data()[141] 3.342s passed
lenOfSeqSub data()[142] 3.331s passed
lenOfSeqReverse data()[143] 3.352s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.344s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.355s passed
getOfSeqSingletonEQ data()[146] 3.330s passed
getOfSeqConcatEQ data()[147] 3.356s passed
getOfSeqSubEQ data()[148] 3.350s passed
getOfSeqReverseEQ data()[149] 3.336s passed
div_exists data()[14] 3.605s passed
lenOfSeqEmptyEQ data()[150] 3.356s passed
lenOfSeqSingletonEQ data()[151] 3.335s passed
lenOfSeqConcatEQ data()[152] 3.351s passed
lenOfSeqSubEQ data()[153] 3.354s passed
lenOfSeqReverseEQ data()[154] 3.331s passed
getOfSeqDefEQ data()[155] 3.350s passed
lenOfSeqDefEQ data()[156] 3.349s passed
seqConcatWithSeqEmpty1 data()[157] 3.335s passed
seqConcatWithSeqEmpty2 data()[158] 3.352s passed
seqReverseOfSeqEmpty data()[159] 3.350s passed
div_one data()[15] 3.387s passed
subSeqComplete data()[160] 3.361s passed
subSeqTailR data()[161] 3.344s passed
subSeqTailL data()[162] 3.358s passed
subSeqTailEQR data()[163] 3.354s passed
subSeqTailEQL data()[164] 3.353s passed
seqDef_split data()[165] 3.385s passed
seqDef_induction_upper data()[166] 3.368s passed
seqDef_induction_upper_concrete data()[167] 3.369s passed
seqDef_induction_lower data()[168] 3.371s passed
seqDef_induction_lower_concrete data()[169] 3.371s passed
jdiv_one data()[16] 3.412s passed
seqDef_split_in_three data()[170] 3.397s passed
seqDef_empty data()[171] 3.352s passed
seqDef_one_summand data()[172] 3.352s passed
seqDef_lower_equals_upper data()[173] 3.352s passed
seqDefOfSeq data()[174] 3.349s passed
seqSelfDefinitionEQ2 data()[175] 3.354s passed
indexOfSeqSingleton data()[176] 3.352s passed
indexOfSeqConcatFirst data()[177] 3.362s passed
indexOfSeqConcatSecond data()[178] 3.361s passed
indexOfSeqSub data()[179] 3.372s passed
div_zero data()[17] 3.413s passed
lenOfArray2seq data()[180] 3.353s passed
getAnyOfArray2seq data()[181] 3.355s passed
getOfArray2seq data()[182] 3.355s passed
getAnyOfNPermInv data()[183] 3.347s passed
seqNPermRange data()[184] 3.419s passed
seqPermTrans data()[185] 3.367s passed
seqPermRefl data()[186] 3.355s passed
seqPermSplit data()[187] 3.348s passed
seqNPermRight data()[188] 3.414s passed
seqPermFromSwap data()[189] 3.380s passed
divResZero1 data()[18] 3.386s passed
seqPermTransAlt0 data()[190] 3.349s passed
seqPermTransAlt1 data()[191] 3.345s passed
seqPermTransAlt2 data()[192] 3.354s passed
seqPermTransAlt3 data()[193] 3.330s passed
seqPermForall data()[194] 3.442s passed
seqPermExists data()[195] 3.392s passed
schiffl_lemma_2 data()[196] 20.820s passed
schiffl_thm_1 data()[197] 4.019s passed
eqSameSeq data()[198] 3.532s passed
divResZero2 data()[19] 3.386s passed
eqTermCut data()[1] 3.888s passed
divResOne1 data()[20] 3.407s passed
divResOne2 data()[21] 3.402s passed
div_cancel1 data()[22] 3.394s passed
div_cancel2 data()[23] 3.355s passed
divAddMultDenom data()[24] 3.401s passed
divMinus data()[25] 3.488s passed
divMinusDenom data()[26] 3.424s passed
divLeastDPos data()[27] 3.357s passed
divLeastDNeg data()[28] 3.353s passed
divGreatestDPos data()[29] 3.372s passed
equivAllRight data()[2] 3.764s passed
divGreatestDNeg data()[30] 3.395s passed
divIncreasingPos data()[31] 3.364s passed
divIncreasingNeg data()[32] 3.372s passed
jdiv_zero data()[33] 3.345s passed
jdivPulloutMinusNum data()[34] 3.372s passed
jdivPulloutMinusDenom data()[35] 3.369s passed
jdiv_uniquePosPos data()[36] 3.352s passed
jdiv_uniquePosNeg data()[37] 3.349s passed
jdiv_uniqueNegPos data()[38] 3.371s passed
jdiv_uniqueNegNeg data()[39] 3.340s passed
irrflConcrete1 data()[3] 3.698s passed
jdivMultDenom1 data()[40] 3.355s passed
jdivMultDenom2 data()[41] 3.343s passed
mod_geZero data()[42] 3.368s passed
mod_lessDenom data()[43] 3.355s passed
jmod_NumPos data()[44] 3.337s passed
jmod_NumNeg data()[45] 3.334s passed
jmod_geZero data()[46] 3.335s passed
jmodNumZero data()[47] 3.365s passed
jmod_pulloutminusNum data()[48] 3.349s passed
jmod_pulloutminusDenom data()[49] 3.349s passed
irrflConcrete2 data()[4] 3.542s passed
jmodUnique1 data()[50] 3.376s passed
jmodUnique2 data()[51] 3.412s passed
intDivRem data()[52] 3.347s passed
jmodjmod data()[53] 3.370s passed
jmodDivisible data()[54] 3.350s passed
jmodDivisibleRep data()[55] 3.351s passed
jdivAddMultDenom data()[56] 3.476s passed
jmodAltZero data()[57] 3.338s passed
jmodAddMultDenomZero data()[58] 3.352s passed
polyDiv_zero data()[59] 3.380s passed
cancel_gtPos data()[5] 3.553s passed
polyMod_ltdivDenom data()[60] 3.345s passed
bsum_empty data()[61] 3.324s passed
bsum_induction_upper data()[62] 3.320s passed
bsum_induction_lower data()[63] 3.337s passed
bsum_num_of_bounds data()[64] 3.361s passed
bsum_num_of_bounds2 data()[65] 3.365s passed
bsum_induction_upper2 data()[66] 3.331s passed
bsum_induction_upper_concrete data()[67] 3.334s passed
bsum_induction_upper_concrete_2 data()[68] 3.350s passed
bsum_induction_upper2_concrete data()[69] 3.324s passed
cancel_gtNeg data()[6] 3.508s passed
bsum_induction_lower_concrete data()[70] 3.332s passed
bsum_induction_lower2 data()[71] 3.329s passed
bsum_induction_lower2_concrete data()[72] 3.337s passed
bsum_positive data()[73] 3.383s passed
bsum_upper_bound data()[74] 3.355s passed
bsum_lower_bound data()[75] 3.345s passed
bsum_positive_lower_bound_element data()[76] 3.357s passed
bsum_sub_same_index data()[77] 3.382s passed
bsum_less_same_index data()[78] 3.362s passed
bsum_equal_except_one_index data()[79] 3.367s passed
moduloIntIsInInt data()[7] 3.438s passed
bsum_num_of_is_max data()[80] 3.347s passed
bsum_num_of_is_max2 data()[81] 3.362s passed
bsum_num_of_is_max3 data()[82] 3.346s passed
bsum_num_of_is_max4 data()[83] 3.342s passed
bsum_num_of_lt_max data()[84] 3.349s passed
bsum_num_of_lt_max2 data()[85] 3.364s passed
bsum_num_of_lt_max3 data()[86] 3.340s passed
bsum_num_of_lt_max4 data()[87] 3.337s passed
bsum_num_of_gt0 data()[88] 3.338s passed
bsum_num_of_gt0_alt data()[89] 3.341s passed
moduloLongIsInLong data()[8] 3.470s passed
bsum_add_concrete data()[90] 3.348s passed
bprod_all_positive data()[91] 3.333s passed
bprod_split data()[92] 3.316s passed
powConcrete0 data()[93] 3.319s passed
powConcrete1 data()[94] 3.350s passed
powSplitFactor data()[95] 3.328s passed
powAdd data()[96] 3.342s passed
powMono data()[97] 3.338s passed
powMonoConcrete data()[98] 3.349s passed
powMonoConcreteRight data()[99] 3.326s passed
moduloShortIsInShort data()[9] 3.412s passed

Standard output

616        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
642        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.91ms 
879        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
897        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)

1812       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1815       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1819       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1819       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3176       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8898       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.02s 
8959       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8992       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.7ns 
9006       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9007       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.35ms 
9011       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11919      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
11922      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12861      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12885      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.6ms 
12898      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12899      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 627.41ns 
12900      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
15725      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16646      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16659      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.97ms 
16663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16666      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.57ms 
16668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19433      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
19434      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20358      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
20361      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20362      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.61ns 
20363      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23001      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
23002      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23901      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 
23905      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23905      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 577.11ns 
23907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26564      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
26564      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27454      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.65ms 
27458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27458      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.21ns 
27460      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30070      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
30071      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30958      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.29ms 
30967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 435.31ns 
30969      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33569      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
33570      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
34398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
34401      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 820.81ns 
34404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34404      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.61ns 
34406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37027      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
37028      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37869      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37872      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 664.11ns 
37874      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37874      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.11ns 
37875      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
40438      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
41284      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.71ns 
41286      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.6ns 
41287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43841      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
43841      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
44683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
44686      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 571.21ns 
44688      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
44688      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.4ns 
44689      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47298      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
47298      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
48117      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
48119      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.11ns 
48121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
48121      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.7ns 
48122      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50792      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
50793      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
51629      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
51664      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.8ms 
51669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
51670      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 765.21ns 
51671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54348      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
54349      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
55186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
55214      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.8ms 
55216      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
55216      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.2ns 
55217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57780      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
57780      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
58617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
58818      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 192.16ms 
58822      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
58822      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.7ns 
58823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61388      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
61388      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
62200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
62206      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
62211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
62211      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.31ns 
62212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64785      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
64786      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
65617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
65621      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
65622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
65623      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112ns 
65623      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68165      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
68165      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
68996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
69033      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.69ms 
69035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
69035      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215ns 
69036      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
71576      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
72406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
72419      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
72422      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
72422      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.41ns 
72423      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74963      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
74963      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
75794      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
75805      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.85ms 
75807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
75807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.1ns 
75808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78384      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
78384      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
79199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
79212      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.36ms 
79214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
79215      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.11ns 
79216      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81773      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
81773      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
82602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
82614      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.77ms 
82616      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
82616      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
82617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85160      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
85161      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
85990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
86008      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.87ms 
86010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
86010      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.9ns 
86011      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88531      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
88532      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
89360      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
89364      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
89365      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
89365      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.2ns 
89366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91925      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
91926      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
92733      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
92764      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.61ms 
92766      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
92766      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.8ns 
92768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95323      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
95323      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
96184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
96249      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.76ms 
96255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
96256      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.9ns 
96258      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98818      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
98818      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
99647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
99677      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.55ms 
99678      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
99678      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 
99679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
102200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
103027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
103034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 
103035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
103036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.6ns 
103036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
105574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
106376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
106387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.53ms 
106389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
106389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.3ns 
106390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
108924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
109750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
109759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.89ms 
109761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
109761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
109762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
112321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
113148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
113154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms 
113155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
113156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
113156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
115674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
116507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
116517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ms 
116527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
116528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 469.61ns 
116529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
119057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
119885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
119891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
119893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
119893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
119893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
122432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
123233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
123237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
123238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
123238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
123239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
125768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
126599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
126608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.29ms 
126609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
126609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.4ns 
126610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
129121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
129945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
129977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.71ms 
129979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
129979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.9ns 
129980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
132491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
133315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
133329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ms 
133331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
133331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.3ns 
133332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
135865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
136666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
136679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.96ms 
136680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
136680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
136681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
139214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
140035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
140050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.74ms 
140051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
140051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
140052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
142555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
143376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
143389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.04ms 
143391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
143391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.2ns 
143392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
145893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
146716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
146744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.61ms 
146746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
146746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
146747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
149279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
150085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
150088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
150089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
150089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
150090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
152631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
153452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
153456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
153457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
153457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
153458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
155979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
156804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
156810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.01ms 
156811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
156811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
156812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
159314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
160141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
160147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
160149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
160149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
160149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
162647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
163466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
163481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.94ms 
163482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
163482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
163483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
166010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
166810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
166816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
166818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
166818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
166818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
169350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
170178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
170181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
170183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
170183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.31ns 
170184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
172703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
173527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
173530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
173531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
173532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
173532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
176053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
176876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
176880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
176881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
176881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.9ns 
176882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
179405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
180204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
180255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.28ms 
180257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
180257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
180258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
182779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
183607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
183667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.03ms 
183669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
183669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
183670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
186186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
187012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
187015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
187016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
187016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
187017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
189531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
190354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
190383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.86ms 
190386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
190386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 437.11ns 
190387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
192917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
193715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
193734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.27ms 
193735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
193736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
193736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
196259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
197083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
197085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 863.22ns 
197087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
197087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.8ns 
197088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
199644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
200466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
200560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83ms 
200563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
200563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.11ns 
200564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
203069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
203891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
203899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.86ms 
203901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
203901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.6ns 
203902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
206440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
207245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
207251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
207253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
207253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.7ns 
207254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
209782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
210608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
210631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.52ms 
210633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
210633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.4ns 
210633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
213144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
213966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
213976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
213978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
213978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
213979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
216481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
217297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
217300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
217302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
217302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.1ns 
217303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
219794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
220616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
220620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
220621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
220621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
220622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
223142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
223943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
223957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.73ms 
223958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
223958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
223959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
226486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
227307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
227318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ms 
227320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
227320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
227320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
229849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
230672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
230683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.09ms 
230684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
230684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
230685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
233189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
234012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
234015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 782.11ns 
234016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
234016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
234017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
236546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
237346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
237349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
237350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
237350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
237351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
239874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
240694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
240699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
240700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
240700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
240701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
243201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
244020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
244023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 767.31ns 
244024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
244024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
244025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
246531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
247353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
247355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 463.72ns 
247356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
247356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
247357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
249861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
250680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
250684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
250685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
250685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
250686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
253215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
254016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
254020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.71ns 
254021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
254022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
254022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
256543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
257370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
257403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.22ms 
257405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
257405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
257406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
259913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
260731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
260758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.29ms 
260760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
260760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
260761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
263260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
264081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
264104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.69ms 
264105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
264105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
264106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
266630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
267430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
267460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.57ms 
267462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
267463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.5ns 
267464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
270004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
270825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
270842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.05ms 
270844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
270844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
270845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
273349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
274172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
274204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.42ms 
274206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
274206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
274207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
276727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
277552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
277570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.23ms 
277574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
277574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.9ns 
277575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
280107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
280906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
280918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.49ms 
280919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
280920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
280920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
283441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
284266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
284281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.42ms 
284282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
284282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
284283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
286793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
287615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
287627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.36ms 
287628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
287628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
287629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
290132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
290952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
290968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.59ms 
290969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
290969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
290970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
293503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
294302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
294317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.83ms 
294318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
294318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
294319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
296840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
297665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
297681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ms 
297682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
297682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
297683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
300186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
301008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
301022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
301023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
301023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
301024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
303524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
304345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
304358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.38ms 
304360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
304360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
304361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
306862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
307682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
307696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.42ms 
307697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
307698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
307698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
310227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
311022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
311037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.73ms 
311038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
311038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
311039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
313560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
314380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
314385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.39ms 
314387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
314387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
314387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
316889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
317708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
317719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ms 
317720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
317720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
317721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
320213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
321031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
321035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
321036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
321036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
321037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
323553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
324351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
324354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 549.11ns 
324355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
324355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
324356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
326881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
327701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
327703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.91ns 
327705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
327705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
327705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
330205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
331026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
331031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.07ms 
331032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
331032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
331033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
333543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
334368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
334373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
334376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
334376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200ns 
334377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
336901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
337701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
337711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.97ms 
337713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
337713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221ns 
337714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
340234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
341057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
341060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
341061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
341061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
341062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
343562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
344384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
344387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 486.81ns 
344388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
344388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
344388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
346891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
347711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
347716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
347717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
347717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
347718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
350216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
351036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
351038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 502.51ns 
351039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
351039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
351040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
353564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
354362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
354364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 477.01ns 
354366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
354366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
354366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
356883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
357703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
357705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 488.51ns 
357707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
357707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
357707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
360204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
361026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
361029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
361030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
361030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
361031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
363527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
364350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
364357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
364358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
364358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
364359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
366880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
367680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
367683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
367684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
367684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
367685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
370217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
371038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
371043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
371044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
371044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
371045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
373544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
374367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
374371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
374372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
374372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
374373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
376877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
377697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
377715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 
377717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
377717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
377718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
380240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
381039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
381042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
381045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
381045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
381046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
383557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
384355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
384358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 987.92ns 
384359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
384359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
384360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
386875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
387696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
387700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
387701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
387701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
387702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
390197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
391017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
391029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 
391031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
391031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
391031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
393526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
394346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
394350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 274.9ns 
394352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
394352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
394352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
396863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
397660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
397685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.52ms 
397686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
397686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
397687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
400198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
401017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
401020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
401021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
401021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
401022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
403515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
404335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
404349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.44ms 
404350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
404351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
404351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
406861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
407659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
407672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.84ms 
407673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
407673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
407674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
410193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
411013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
411030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.41ms 
411032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
411032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
411033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
413527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
414352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
414354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 514.51ns 
414357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
414357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.6ns 
414358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
416854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
417675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
417680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
417681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
417681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
417682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
420193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
421017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
421020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
421021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
421021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
421022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
423518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
424342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
424345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.21ns 
424346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
424346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
424346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
426841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
427670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
427673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 669.51ns 
427674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
427674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
427675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
430190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
431017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
431020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
431021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
431021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
431021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
433514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
434341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
434343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
434344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
434345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
434345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
436855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
437662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
437669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
437670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
437670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
437671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
440187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
441013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
441020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
441021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
441021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
441022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
443517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
444347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
444353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 
444355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
444355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
444356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
446879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
447694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
447701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
447703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
447704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.7ns 
447704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
450227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
451062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
451066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
451067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
451067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
451068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
453583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
454393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
454397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
454398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
454398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
454399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
456928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
457759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
457761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.81ns 
457762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
457762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
457763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
460249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
461079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
461082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 923.82ns 
461083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
461083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
461084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
463593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
464425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
464428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 867.21ns 
464429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
464430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.6ns 
464430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
466930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
467762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
467771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.45ms 
467772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
467772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
467773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
470297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
471127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
471130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
471131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
471131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
471132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
473628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
474463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
474468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
474469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
474469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
474470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
476986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
477817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
477819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 773.51ns 
477820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
477820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
477821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
480320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
481151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
481153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 572.91ns 
481155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
481155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
481155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
483663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
484493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
484495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
484497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
484497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
484497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
486993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
487824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
487826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.01ns 
487827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
487827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
487828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
490344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
491176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
491178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 994.12ns 
491179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
491179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
491180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
493688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
494520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
494522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 916.72ns 
494523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
494523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
494524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
497043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
497874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
497877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
497878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
497879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
497879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
500393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
501205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
501207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 859.31ns 
501209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
501209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
501209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
503723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
504556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
504564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.01ms 
504565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
504565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
504565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
507079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
507912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
507914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 498.21ns 
507915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
507915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
507916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
510413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
511244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
511249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
511251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
511251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
511252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
513770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
514603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
514606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 837.81ns 
514607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
514607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
514608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
517126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
517938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
517940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.81ns 
517941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
517941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
517942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
520456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
521288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
521292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
521293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
521293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
521294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
523809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
524643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
524646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 814.31ns 
524647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
524647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
524647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
527162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
527974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
527977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
527978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
527978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
527978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
530490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
531324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
531326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
531327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
531328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
531328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
533841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
534671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
534675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
534676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
534676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
534678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
537189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
538004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
538011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
538012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
538012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
538013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
540523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
541354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
541362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
541363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
541363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
541364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
543875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
544706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
544712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
544713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
544713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
544715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
547233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
548067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
548073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.91ms 
548074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
548074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
548075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
550593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
551407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
551417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.62ms 
551419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
551419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
551419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
553931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
554764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
554775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.04ms 
554777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
554777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.1ns 
554778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
557287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
558120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
558129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.94ms 
558130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
558130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
558131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
560644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
561476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
561482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
561484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
561484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
561484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
563995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
564849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
564867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.01ms 
564868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
564868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
564869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
567380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
568216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
568236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.44ms 
568237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
568237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
568238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
570751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
571587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
571605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.66ms 
571606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
571606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
571607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
574123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
574958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
574975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.23ms 
574976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
574977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
574977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
577493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
578328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
578346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.97ms 
578348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
578348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
578348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
580859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
581698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
581743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.39ms 
581745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
581745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
581745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
584251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
585087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
585095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.78ms 
585097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
585097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
585097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
587609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
588443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
588448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
588449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
588449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
588450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
590962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
591796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
591799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
591801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
591801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
591801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
594326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
595137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
595149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.11ms 
595150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
595150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
595151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
597683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
598497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
598503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
598504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
598504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
598505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
601016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
601851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
601854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
601855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
601855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
601856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
604373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
605207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
605216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.04ms 
605217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
605217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
605218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
607732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
608568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
608577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.56ms 
608579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
608579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
608579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
611100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
611937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
611949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.82ms 
611951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
611951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
611951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
614467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
615300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
615303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 978.02ns 
615304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
615304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.3ns 
615305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
617818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
618654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
618657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
618659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
618659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
618659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
621174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
622008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
622013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.63ms 
622014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
622014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
622015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
624523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
625355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
625359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
625360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
625360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
625361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
627888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
628702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
628778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.31ms 
628780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
628781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.1ns 
628781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
631285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
632123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
632144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.36ms 
632147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
632147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.61ns 
632148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
634658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
635490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
635501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
635502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
635502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
635503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
638014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
638846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
638848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 162.2ns 
638849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
638849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
638851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
641354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
642185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
642262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.43ms 
642264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
642264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
642265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
644774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
645610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
645642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.91ms 
645644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
645644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
645645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
648156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
648989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
648991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 221.4ns 
648992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
648992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
648993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
651504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
652335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
652337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 190.6ns 
652338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
652338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
652338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
654855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
655688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
655690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 242.6ns 
655691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
655691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
655692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
658189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
659018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
659020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 391.91ns 
659021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
659021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
659022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
661518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
662353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
662446     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
662462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.57ms 
662464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
662465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.4ns 
662466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
664980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
665813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
665853     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
665855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.37ms 
665856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
665856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.7ns 
665857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
668364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
669216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
669218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 
669247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
669301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
669313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
669317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
669327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
669327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
669329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
669330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
669334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
669336     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' 
669337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
669339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
669532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
669533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
669536     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' 
669538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
669540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
669657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
669658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
669659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
669660     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' 
669661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
669662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
669826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
669827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
669828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
669829     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' 
669830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
669831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
669950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
669952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
669953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
669954     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' 
669954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
669955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
669962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
669963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
669964     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' 
669965     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' 
669965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
669966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
669973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
669974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
669975     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' 
669975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
669976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
669977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
670099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
670099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
670100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
670207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
670208     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)'' 
670209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
670212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
670213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
670213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
670214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
670215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
670218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
670219     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' 
670220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
670221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
670222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
670315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
670318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
670319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
670320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
670322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
670322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
670326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
670435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
670436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
670437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
670439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
670440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
670440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
670441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
670442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
670534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
670536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
670609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
670613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
670618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
670619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
670622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
670623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
670624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
670625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
670625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
670626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
670633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
670637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
670718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
670719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
670721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
670722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
670723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
670724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
670724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
670725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
670769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
670775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
670854     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]'' 
670855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
670856     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'' 
670857     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'' 
670858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
670859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
670990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
670994     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'' 
670996     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)'' 
670997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
670999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
670999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
671000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
671000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
671011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
671016     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'' 
671017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
671018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
671102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
671104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
671105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
671106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
671106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
671107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
671197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
671198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
671200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
671201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
671201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
671202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
671203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
671204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
671277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
671280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
671354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
671354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
671356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
671361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
671364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
671369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
671475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
671476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
671477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
671478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
671487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
671563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
674770     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'' 
674770     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)'' 
674774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
674776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
674776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
674777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
674778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
674785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
674787     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'' 
674788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
674789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
674789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
674883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
674886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
674887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
674888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
674889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
674889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
674890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
674980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
674981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
674982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
674986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
674986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
674987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
674988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
674988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
675064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
675065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
675139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
675143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
675147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
675148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
675149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
675150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
675159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
675241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
675242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
675243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
675244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
675355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
675364     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'' 
675365     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)'' 
675366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
675367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
675368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
675369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
675369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
675379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
675380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
675381     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'' 
675382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
675383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
675464     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))'' 
675465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
675466     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'' 
675467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
675468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
675552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
675556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
675557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
675558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
675559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
675559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
675560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
675652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
675653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
675654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
675655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
675656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
675656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
675657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
675658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
675659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
675659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
675660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
675661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
675662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
675662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
675663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
675744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
675746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
675752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
675823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
675898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
675899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
675900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
675901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
675901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
675902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
675902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
675903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
675903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
675981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
675987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
676069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
676070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
676071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
676071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
676072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
676072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
676073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
676073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
676078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
676078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
676151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
676156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
676161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
676254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
676255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
676255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
676256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
676257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
676257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
676257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
676258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
676308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
676309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
676310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
676310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
676311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
676316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
676321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
676432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
676514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
676514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
676515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
676516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
676671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
676754     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'' 
676754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
679553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
679557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
679558     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'' 
679559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
679560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
679667     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))'' 
679667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
679668     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'' 
679669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
679670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
679768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
682501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
685474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
685477     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'' 
685478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
685479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
685480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
685587     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))'' 
685588     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'' 
685588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
685589     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)' ...' 
685590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
686675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
686675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
686676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
689246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
690104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
690105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
690106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
690112     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)'' 
690120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
690122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
690124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
690125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
690129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
690130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
690133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
690133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
690136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
690144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
690145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
690146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
690240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
690240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
690241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
690241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
690242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
690298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
690298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
690299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
690300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
690300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
690303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
690303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
690304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
690304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
690305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
690306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
690372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
690372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
690372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
690373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
690374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
690374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
690435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
690436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
690437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
690437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
690437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
690438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
690438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
690439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
690439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
690440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
690440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
690440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
690441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
690441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
690441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
690442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
690442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
690442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
690443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
690445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
690471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
690472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
690512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
690513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
690513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
690514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
690515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
690516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
690552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
690554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
690555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
690556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
690557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
690557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
690558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
690596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
690598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
690600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
690647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
690695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
690695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
690696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
693271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
694208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
694225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms