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

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

tests
0

failures
0

ignored
11m36.68s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.381s passed
powPositiveConcrete data()[101] 3.355s passed
powGeq1Concrete data()[102] 3.350s passed
pow2InIntLower data()[103] 3.359s passed
pow2InIntUpper data()[104] 3.365s passed
logSelfConcrete data()[105] 3.389s passed
log1Concrete data()[106] 3.374s passed
logProduct data()[107] 3.387s passed
logTimesBaseConcrete data()[108] 3.390s passed
logProdIdentity data()[109] 3.392s passed
moduloByteIsInByte data()[10] 3.474s passed
logProdIdentityConcrete data()[110] 3.444s passed
logPowIdentity data()[111] 3.334s passed
logPowIdentityConcrete data()[112] 3.390s passed
logPositive data()[113] 3.388s passed
logPositiveConcrete data()[114] 3.350s passed
logMono data()[115] 3.405s passed
logMonoConcrete data()[116] 3.378s passed
powLogLess data()[117] 3.401s passed
powLogMore2 data()[118] 3.375s passed
logLessThanPow data()[119] 3.396s passed
moduloCharIsInChar data()[11] 3.448s passed
logLessThanPowConcrete data()[120] 3.354s passed
logSqueeze data()[121] 3.356s passed
ifthenelse_equals data()[122] 3.383s passed
ifthenelse_equals_1 data()[123] 3.379s passed
ifthenelse_equals_2 data()[124] 3.360s passed
disjointWithSingleton1 data()[125] 3.371s passed
disjointWithSingleton2 data()[126] 3.373s passed
disjointArrayRanges data()[127] 3.563s passed
disjointArrayRangeAllFields1 data()[128] 3.400s passed
disjointArrayRangeAllFields2 data()[129] 3.393s passed
div_unique1 data()[12] 3.488s passed
seqSelfDefinition data()[130] 3.417s passed
seqOutsideValue data()[131] 3.368s passed
castedGetAny data()[132] 3.363s passed
seqGetAlphaCast data()[133] 3.359s passed
getOfSeqSingleton data()[134] 3.362s passed
getOfSeqSingletonConcrete data()[135] 3.377s passed
getOfSeqConcat data()[136] 3.395s passed
getOfSeqSub data()[137] 3.378s passed
getOfSeqReverse data()[138] 3.390s passed
lenOfSeqEmpty data()[139] 3.360s passed
div_unique2 data()[13] 3.438s passed
lenOfSeqSingleton data()[140] 3.390s passed
lenOfSeqConcat data()[141] 3.436s passed
lenOfSeqSub data()[142] 3.392s passed
lenOfSeqReverse data()[143] 3.367s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.387s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.426s passed
getOfSeqSingletonEQ data()[146] 3.386s passed
getOfSeqConcatEQ data()[147] 3.426s passed
getOfSeqSubEQ data()[148] 3.399s passed
getOfSeqReverseEQ data()[149] 3.360s passed
div_exists data()[14] 3.602s passed
lenOfSeqEmptyEQ data()[150] 3.367s passed
lenOfSeqSingletonEQ data()[151] 3.395s passed
lenOfSeqConcatEQ data()[152] 3.389s passed
lenOfSeqSubEQ data()[153] 3.388s passed
lenOfSeqReverseEQ data()[154] 3.347s passed
getOfSeqDefEQ data()[155] 3.387s passed
lenOfSeqDefEQ data()[156] 3.357s passed
seqConcatWithSeqEmpty1 data()[157] 3.406s passed
seqConcatWithSeqEmpty2 data()[158] 3.401s passed
seqReverseOfSeqEmpty data()[159] 3.398s passed
div_one data()[15] 3.496s passed
subSeqComplete data()[160] 3.378s passed
subSeqTailR data()[161] 3.414s passed
subSeqTailL data()[162] 3.423s passed
subSeqTailEQR data()[163] 3.405s passed
subSeqTailEQL data()[164] 3.417s passed
seqDef_split data()[165] 3.492s passed
seqDef_induction_upper data()[166] 3.454s passed
seqDef_induction_upper_concrete data()[167] 3.433s passed
seqDef_induction_lower data()[168] 3.437s passed
seqDef_induction_lower_concrete data()[169] 3.442s passed
jdiv_one data()[16] 3.462s passed
seqDef_split_in_three data()[170] 3.518s passed
seqDef_empty data()[171] 3.435s passed
seqDef_one_summand data()[172] 3.392s passed
seqDef_lower_equals_upper data()[173] 3.371s passed
seqDefOfSeq data()[174] 3.397s passed
seqSelfDefinitionEQ2 data()[175] 3.392s passed
indexOfSeqSingleton data()[176] 3.382s passed
indexOfSeqConcatFirst data()[177] 3.409s passed
indexOfSeqConcatSecond data()[178] 3.398s passed
indexOfSeqSub data()[179] 3.390s passed
div_zero data()[17] 3.449s passed
lenOfArray2seq data()[180] 3.379s passed
getAnyOfArray2seq data()[181] 3.427s passed
getOfArray2seq data()[182] 3.499s passed
getAnyOfNPermInv data()[183] 3.392s passed
seqNPermRange data()[184] 3.426s passed
seqPermTrans data()[185] 3.572s passed
seqPermRefl data()[186] 3.509s passed
seqPermSplit data()[187] 3.474s passed
seqNPermRight data()[188] 3.775s passed
seqPermFromSwap data()[189] 3.450s passed
divResZero1 data()[18] 3.438s passed
seqPermTransAlt0 data()[190] 3.419s passed
seqPermTransAlt1 data()[191] 3.376s passed
seqPermTransAlt2 data()[192] 3.389s passed
seqPermTransAlt3 data()[193] 3.427s passed
seqPermForall data()[194] 3.506s passed
seqPermExists data()[195] 3.430s passed
schiffl_lemma_2 data()[196] 22.249s passed
schiffl_thm_1 data()[197] 4.164s passed
eqSameSeq data()[198] 3.541s passed
divResZero2 data()[19] 3.468s passed
eqTermCut data()[1] 4.042s passed
divResOne1 data()[20] 3.440s passed
divResOne2 data()[21] 3.432s passed
div_cancel1 data()[22] 3.467s passed
div_cancel2 data()[23] 3.391s passed
divAddMultDenom data()[24] 3.435s passed
divMinus data()[25] 3.457s passed
divMinusDenom data()[26] 3.450s passed
divLeastDPos data()[27] 3.460s passed
divLeastDNeg data()[28] 3.412s passed
divGreatestDPos data()[29] 3.399s passed
equivAllRight data()[2] 3.761s passed
divGreatestDNeg data()[30] 3.400s passed
divIncreasingPos data()[31] 3.365s passed
divIncreasingNeg data()[32] 3.393s passed
jdiv_zero data()[33] 3.392s passed
jdivPulloutMinusNum data()[34] 3.407s passed
jdivPulloutMinusDenom data()[35] 3.471s passed
jdiv_uniquePosPos data()[36] 3.444s passed
jdiv_uniquePosNeg data()[37] 3.373s passed
jdiv_uniqueNegPos data()[38] 3.411s passed
jdiv_uniqueNegNeg data()[39] 3.430s passed
irrflConcrete1 data()[3] 3.698s passed
jdivMultDenom1 data()[40] 3.411s passed
jdivMultDenom2 data()[41] 3.418s passed
mod_geZero data()[42] 3.375s passed
mod_lessDenom data()[43] 3.388s passed
jmod_NumPos data()[44] 3.378s passed
jmod_NumNeg data()[45] 3.471s passed
jmod_geZero data()[46] 3.397s passed
jmodNumZero data()[47] 3.469s passed
jmod_pulloutminusNum data()[48] 3.513s passed
jmod_pulloutminusDenom data()[49] 3.370s passed
irrflConcrete2 data()[4] 3.575s passed
jmodUnique1 data()[50] 3.418s passed
jmodUnique2 data()[51] 3.482s passed
intDivRem data()[52] 3.368s passed
jmodjmod data()[53] 3.436s passed
jmodDivisible data()[54] 3.401s passed
jmodDivisibleRep data()[55] 3.369s passed
jdivAddMultDenom data()[56] 3.508s passed
jmodAltZero data()[57] 3.386s passed
jmodAddMultDenomZero data()[58] 3.424s passed
polyDiv_zero data()[59] 3.423s passed
cancel_gtPos data()[5] 3.557s passed
polyMod_ltdivDenom data()[60] 3.363s passed
bsum_empty data()[61] 3.360s passed
bsum_induction_upper data()[62] 3.370s passed
bsum_induction_lower data()[63] 3.394s passed
bsum_num_of_bounds data()[64] 3.406s passed
bsum_num_of_bounds2 data()[65] 3.382s passed
bsum_induction_upper2 data()[66] 3.352s passed
bsum_induction_upper_concrete data()[67] 3.368s passed
bsum_induction_upper_concrete_2 data()[68] 3.384s passed
bsum_induction_upper2_concrete data()[69] 3.431s passed
cancel_gtNeg data()[6] 3.524s passed
bsum_induction_lower_concrete data()[70] 3.349s passed
bsum_induction_lower2 data()[71] 3.400s passed
bsum_induction_lower2_concrete data()[72] 3.365s passed
bsum_positive data()[73] 3.403s passed
bsum_upper_bound data()[74] 3.433s passed
bsum_lower_bound data()[75] 3.409s passed
bsum_positive_lower_bound_element data()[76] 3.407s passed
bsum_sub_same_index data()[77] 3.405s passed
bsum_less_same_index data()[78] 3.435s passed
bsum_equal_except_one_index data()[79] 3.398s passed
moduloIntIsInInt data()[7] 3.509s passed
bsum_num_of_is_max data()[80] 3.378s passed
bsum_num_of_is_max2 data()[81] 3.417s passed
bsum_num_of_is_max3 data()[82] 3.429s passed
bsum_num_of_is_max4 data()[83] 3.400s passed
bsum_num_of_lt_max data()[84] 3.399s passed
bsum_num_of_lt_max2 data()[85] 3.424s passed
bsum_num_of_lt_max3 data()[86] 3.374s passed
bsum_num_of_lt_max4 data()[87] 3.399s passed
bsum_num_of_gt0 data()[88] 3.381s passed
bsum_num_of_gt0_alt data()[89] 3.411s passed
moduloLongIsInLong data()[8] 3.433s passed
bsum_add_concrete data()[90] 3.365s passed
bprod_all_positive data()[91] 3.398s passed
bprod_split data()[92] 3.417s passed
powConcrete0 data()[93] 3.402s passed
powConcrete1 data()[94] 3.368s passed
powSplitFactor data()[95] 3.385s passed
powAdd data()[96] 3.353s passed
powMono data()[97] 3.401s passed
powMonoConcrete data()[98] 3.373s passed
powMonoConcreteRight data()[99] 3.348s passed
moduloShortIsInShort data()[9] 3.452s passed

Standard output

683        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
705        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.63ms 
920        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
934        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)

1758       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1760       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1761       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1762       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3042       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8665       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.74s 
8725       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8755       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.3ns 
8767       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8767       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.8ns 
8772       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11810      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
11812      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12801      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.82ms 
12814      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12814      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.9ns 
12815      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15616      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
15616      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16544      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16571      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.32ms 
16575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.9ns 
16580      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19390      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
19390      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20264      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20271      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
20273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20273      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.7ns 
20275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22944      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
22944      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23846      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
23847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23848      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.3ns 
23849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26467      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
26467      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27362      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27403      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.77ms 
27405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27405      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.1ns 
27406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30025      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
30025      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30927      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.14ms 
30929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30929      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.1ns 
30930      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33537      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
33537      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
34433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
34436      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.7ns 
34438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34439      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.4ns 
34440      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
37022      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37867      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37870      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.8ns 
37871      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37871      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.8ns 
37872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40467      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
40468      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
41321      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 575.8ns 
41323      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41323      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.3ns 
41324      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43942      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
43943      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
44791      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
44794      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.6ns 
44797      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
44797      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.8ns 
44798      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47396      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
47396      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
48241      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
48243      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 548.7ns 
48245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
48245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
48246      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50843      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
50844      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
51684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
51729      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.03ms 
51733      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
51733      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.3ns 
51734      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54316      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
54316      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
55136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
55169      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.09ms 
55171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
55171      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.2ns 
55172      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57737      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
57737      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
58577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
58768      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 182.82ms 
58774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
58774      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.1ns 
58775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61387      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
61388      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
62260      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
62268      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
62272      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
62272      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.2ns 
62273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64875      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
64876      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
65728      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
65731      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
65734      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
65735      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.3ns 
65736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68307      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
68308      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
69145      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
69181      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.86ms 
69184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
69184      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.6ns 
69185      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71756      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
71757      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
72599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
72619      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.07ms 
72621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
72622      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.2ns 
72623      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75216      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
75216      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
76073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
76086      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.58ms 
76089      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
76089      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.8ns 
76090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78665      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
78666      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
79512      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
79527      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.17ms 
79528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
79528      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
79529      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82105      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
82105      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
82945      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
82960      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.69ms 
82961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
82961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.5ns 
82962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85563      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
85563      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
86402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
86426      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.71ms 
86428      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
86428      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.6ns 
86429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88983      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
88983      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
89814      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
89817      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
89820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
89820      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.2ns 
89821      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92373      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
92375      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
93214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
93252      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.59ms 
93255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
93255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.7ns 
93257      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95819      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
95819      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
96658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
96710      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.04ms 
96711      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
96712      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.7ns 
96713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99282      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
99282      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
100097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
100159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.96ms 
100165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
100167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.78ms 
100168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
102781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
103613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
103621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 
103622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
103622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
103623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
106183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
107021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
107033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.93ms 
107034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
107034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.2ns 
107035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
109592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
110422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
110433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.49ms 
110434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
110434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
110435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
112997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
113826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
113833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
113834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
113834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.6ns 
113835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
116378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
117189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
117197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.51ms 
117199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
117199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.2ns 
117200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
119739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
120583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
120590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.87ms 
120592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
120592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.6ns 
120593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
123147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
123979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
123982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
123984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
123984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.9ns 
123985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
126544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
127376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
127389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.93ms 
127391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
127391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
127392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
129962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
130802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
130860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.87ms 
130862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
130862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.2ns 
130863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
133446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
134287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
134304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.94ms 
134305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
134306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.4ns 
134306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
136832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
137659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
137677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.66ms 
137679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
137680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.1ns 
137681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
140231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
141070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
141089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.4ms 
141090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
141090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
141091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
143663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
144502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
144518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.39ms 
144520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
144520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
144521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
147059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
147892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
147929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.25ms 
147930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
147930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
147931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
150510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
151344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
151347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
151349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
151349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
151349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
153893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
154719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
154723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
154724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
154724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
154725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
157261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
158103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
158111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ms 
158112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
158112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
158113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
160673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
161480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
161488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
161489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
161490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
161490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
164110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
164942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
164960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.01ms 
164961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
164961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
164962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
167521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
168349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
168356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
168357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
168357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
168358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
170926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
171822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
171825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
171827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
171827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.1ns 
171828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
174502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
175334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
175338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
175340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
175340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
175341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
177897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
178704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
178708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
178709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
178709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
178710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
181235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
182058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
182126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.11ms 
182129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
182129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.3ns 
182130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
184679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
185513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
185608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.72ms 
185614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
185614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.3ns 
185615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
188144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
188975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
188978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
188980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
188980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.5ns 
188981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
191547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
192380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
192413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.17ms 
192416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
192416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 417.4ns 
192417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
194962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
195786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
195814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.87ms 
195816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
195816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
195817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
198355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
199182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
199185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
199186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
199186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
199187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
201726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
202554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
202692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127.56ms 
202694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
202694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.3ns 
202695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
205251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
206063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
206078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.29ms 
206079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
206079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
206083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
208655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
209495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
209502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms 
209504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
209504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
209505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
212058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
212910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
212925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ms 
212926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
212926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
212927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
215457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
216277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
216288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.18ms 
216290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
216290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
216290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
218809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
219644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
219648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
219650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
219650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
219651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
222206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
223014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
223019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
223020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
223020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
223021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
225564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
226390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
226412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.92ms 
226413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
226414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
226414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
228974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
229803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
229819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.92ms 
229820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
229820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
229821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
232356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
233183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
233200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.48ms 
233202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
233202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
233202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
235727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
236549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
236553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
236554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
236554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
236554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
239107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
239916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
239921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
239922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
239922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
239923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
242470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
243297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
243304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
243306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
243306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.2ns 
243307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
245889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
246732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
246735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
246736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
246736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
246737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
249261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
250083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
250085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644ns 
250086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
250086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
250087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
252653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
253481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
253484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
253486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
253486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
253486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
256019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
256845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
256848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
256850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
256850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
256851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
259376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
260207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
260252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.66ms 
260254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
260254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.6ns 
260255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
262804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
263643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
263685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.9ms 
263687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
263687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.8ns 
263688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
266258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
267062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
267094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.69ms 
267095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
267095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
267096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
269634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
270455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
270501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.23ms 
270502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
270502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
270503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
273053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
273877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
273906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.96ms 
273907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
273907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
273908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
276459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
277292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
277342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.56ms 
277343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
277343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
277344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
279889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
280712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
280739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.97ms 
280740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
280741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
280741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
283291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
284097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
284117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.47ms 
284119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
284119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.9ns 
284120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
286683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
287510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
287535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.24ms 
287536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
287536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
287537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
290105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
290945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
290964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.94ms 
290965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
290965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
290966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
293508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
294336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
294363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.7ms 
294364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
294364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
294365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
296913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
297738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
297763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.77ms 
297764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
297764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
297765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
300308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
301162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
301186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.76ms 
301187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
301187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
301188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
303715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
304536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
304560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.59ms 
304561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
304562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
304562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
307113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
307940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
307959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.39ms 
307961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
307961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
307961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
310509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
311318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
311341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.32ms 
311342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
311342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
311343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
313900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
314728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
314752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.33ms 
314754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
314754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
314755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
317288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
318109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
318116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.09ms 
318117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
318117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
318118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
320629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
321496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
321514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.38ms 
321515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
321515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
321516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
324087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
324926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
324932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
324934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
324934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.6ns 
324935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
327520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
328331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
328333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540ns 
328334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
328334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
328335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
330878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
331699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
331702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 678.11ns 
331703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
331703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
331703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
334241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
335080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
335086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms 
335087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
335087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
335088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
337607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
338433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
338439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
338441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
338441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187ns 
338442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
341004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
341829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
341840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.32ms 
341841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
341841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
341842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
344379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
345210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
345213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
345215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
345215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
345216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
347731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
348560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
348562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 486.9ns 
348563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
348563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
348564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
351115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
351937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
351942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
351943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
351943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
351944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
354468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
355295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
355297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.8ns 
355298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
355298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
355299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
357838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
358645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
358647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 509ns 
358648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
358648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
358649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
361175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
362004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
362007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.5ns 
362009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
362009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.2ns 
362009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
364539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
365367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
365371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
365372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
365372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
365373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
367916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
368747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
368760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.01ms 
368761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
368761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
368762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
371304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
372131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
372135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
372136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
372136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
372136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
374665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
375515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
375522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
375523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
375523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
375524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
378076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
378908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
378911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
378913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
378913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
378913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
381464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
382289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
382303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.17ms 
382304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
382305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
382305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
384912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
385718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
385747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.45ms 
385748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
385748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 
385749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
388254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
389079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
389082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
389083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
389083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
389083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
391632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
392468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
392472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
392473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
392473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
392474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
395021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
395843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
395859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.71ms 
395860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
395860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
395861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
398383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
399205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
399209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 506.9ns 
399211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
399212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.7ns 
399212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
401750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
402576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
402614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.33ms 
402615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
402615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
402616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
405162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
405989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
405993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
405994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
405994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
405994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
408539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
409371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
409393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.45ms 
409396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
409396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.2ns 
409397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
411937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
412748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
412768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.66ms 
412769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
412769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
412770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
415318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
416141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
416164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.16ms 
416165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
416165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
416166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
418688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
419516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
419519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617ns 
419520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
419520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
419520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
422047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
422869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
422874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
422875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
422875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
422876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
425423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
426254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
426258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
426260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
426261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.2ns 
426261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
428806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
429635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
429638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 773.9ns 
429639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
429639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.4ns 
429639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
432165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
432995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
432997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811ns 
433000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
433000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.2ns 
433001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
435535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
436367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
436370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
436371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
436371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
436371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
438894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
439739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
439742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
439744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
439744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
439746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
442414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
443295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
443305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.46ms 
443306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
443306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
443307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
445860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
446694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
446706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.83ms 
446707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
446707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
446708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
449254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
450087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
450098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
450099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
450100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
450100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
452660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
453472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
453515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.33ms 
453517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
453517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.9ns 
453518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
456049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
456880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
456884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
456885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
456885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
456886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
459405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
460240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
460246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
460247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
460247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
460248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
462770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
463603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
463605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703.8ns 
463606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
463606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
463607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
466131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
466965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
466968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
466969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
466969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
466970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
469505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
470342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
470344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.2ns 
470345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
470346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
470346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
472892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
473729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
473739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 
473740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
473740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
473741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
476299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
477113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
477117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
477119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
477119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.2ns 
477120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
479668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
480502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
480508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
480509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
480509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
480510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
483036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
483866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
483868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.5ns 
483870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
483870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
483870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
486420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
487255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
487257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 614.2ns 
487258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
487258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
487259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
489856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
490690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
490694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
490695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
490695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
490696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
493238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
494082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
494085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
494086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
494086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
494087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
496614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
497450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
497453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
497454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
497454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
497454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
500002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
500837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
500840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
500841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
500841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
500842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
503427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
504260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
504265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
504267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
504267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
504268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
506810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
507648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
507651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
507652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
507652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
507653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
510229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
511067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
511077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
511078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
511078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
511079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
513638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
514474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
514477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.9ns 
514478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
514478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
514478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
517000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
517830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
517836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
517837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
517837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
517838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
520364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
521202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
521204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 872.6ns 
521205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
521205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
521206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
523761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
524596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
524598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 772.2ns 
524599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
524599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
524600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
527151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
527983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
527988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
527989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
527989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
527990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
530544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
531372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
531375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
531377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
531377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.6ns 
531377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
533892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
534719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
534722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
534723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
534724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
534724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
537252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
538106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
538110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
538111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
538111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
538111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
540627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
541462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
541467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
541468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
541468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
541469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
544006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
544858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
544873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms 
544874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
544874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
544874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
547419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
548258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
548273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.52ms 
548274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
548274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
548275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
550823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
551662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
551672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
551673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
551673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
551674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
554203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
555038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
555050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.26ms 
555051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
555051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
555052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
557604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
558439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
558463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.57ms 
558464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
558464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
558465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
561003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
561838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
561862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.82ms 
561888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
561888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
561889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
564427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
565268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
565292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.72ms 
565293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
565294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.6ns 
565294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
567854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
568694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
568708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 
568709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
568710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
568710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
571296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
572136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
572200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.57ms 
572202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
572202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.5ns 
572203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
574745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
575603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
575654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.4ms 
575655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
575655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
575656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
578216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
579050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
579087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.52ms 
579089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
579089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172ns 
579090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
581645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
582485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
582525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.01ms 
582526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
582526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
582527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
585068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
585924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
585966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.65ms 
585968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
585968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
585969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
588506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
589366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
589484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.11ms 
589485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
589485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
589486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
592068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
592911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
592919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.84ms 
592920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
592920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
592921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
595469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
596304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
596311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.75ms 
596312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
596312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
596313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
598841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
599674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
599682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
599683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
599683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
599684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
602228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
603062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
603079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.2ms 
603080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
603080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
603081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
605609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
606461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
606471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.62ms 
606472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
606472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
606473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
609013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
609850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
609853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
609854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
609854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
609855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
612410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
613246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
613262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ms 
613263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
613263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
613264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
615812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
616645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
616660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.25ms 
616661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
616661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
616662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
619199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
620033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
620051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.53ms 
620052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
620052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
620053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
622589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
623427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
623430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
623431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
623431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
623432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
626016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
626852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
626856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 
626857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
626857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
626858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
629514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
630349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
630355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 
630356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
630356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
630357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
632908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
633741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
633747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
633748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
633748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
633749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
636274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
637107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
637173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.18ms 
637175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
637175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
637175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
639836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
640719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
640746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.57ms 
640747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
640748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.6ns 
640748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
643366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
644233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
644255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.01ms 
644256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
644256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
644256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
646847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
647726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
647728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 247.3ns 
647729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
647729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
647730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
650398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
651257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
651503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 236.94ms 
651505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
651506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.8ns 
651506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
654057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
654901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
654953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.17ms 
654954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
654954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
654955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
657535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
658371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
658373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 312.1ns 
658375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
658375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.4ns 
658376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
660912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
661747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
661749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 311.8ns 
661750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
661750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
661751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
664294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
665136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
665138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 352.8ns 
665139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
665139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
665140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
667719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
668562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
668564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 450.4ns 
668565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
668565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
668566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
671137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
671974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
672057     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
672070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.03ms 
672073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
672073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.2ns 
672074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
674609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
675449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
675499     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
675500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.04ms 
675501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
675502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
675507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
678097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
678940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
678941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ns 
678965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
679007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
679032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
679040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
679048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
679051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
679052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
679055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
679061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
679063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
679068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
679070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
679297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
679299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
679300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
679301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
679302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
679414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
679415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
679416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
679417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
679418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
679419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
679576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
679582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
679583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
679584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
679589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
679590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
679698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
679699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
679700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
679701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
679702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
679702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
679709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
679709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
679710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
679712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
679713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
679714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
679719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
679720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
679721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
679722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
679722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
679723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
679853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
679854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
679855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
679965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
679967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
679969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
679970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
679971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
679972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
679973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
679974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
679980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
679982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
679983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
679984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
679985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
680110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
680113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
680114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
680115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
680116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
680117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
680118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
680252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
680254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
680255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
680256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
680257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
680258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
680258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
680260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
680342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
680344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
680453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
680457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
680461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
680462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
680463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
680464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
680465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
680465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
680466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
680467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
680474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
680478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
680570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
680572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
680573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
680574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
680574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
680575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
680575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
680576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
680647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
680652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
680737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
680739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
680740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
680742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
680743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
680743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
680868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
680872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
680873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
680875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
680876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
680877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
680877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
680878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
680886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
680887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
680889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
680889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
680986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
680987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
680988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
680990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
680990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
680991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
681098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
681099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
681100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
681101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
681103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
681104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
681104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
681105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
681191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
681193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
681266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
681267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
681267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
681272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
681276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
681281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
681406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
681412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
681413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
681414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
681425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
681511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
684988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
684989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
684994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
684995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
684996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
684997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
684997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
685005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
685007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
685008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
685009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
685010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
685099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
685103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
685104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
685105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
685106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
685106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
685107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
685198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
685199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
685200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
685201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
685202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
685203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
685203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
685204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
685280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
685282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
685361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
685366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
685370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
685371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
685372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
685372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
685382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
685469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
685470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
685470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
685471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
685598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
685607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
685608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
685610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
685611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
685612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
685613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
685613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
685623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
685625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
685626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
685626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
685627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
685712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
685714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
685715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
685716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
685716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
685804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
685809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
685810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
685811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
685811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
685812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
685813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
685908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
685909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
685910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
685911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
685912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
685913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
685913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
685914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
685915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
685916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
685917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
685918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
685918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
685918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
685919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
686004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
686005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
686011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
686087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
686165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
686167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
686168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
686169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
686170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
686170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
686171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
686171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
686172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
686256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
686262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
686350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
686352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
686353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
686354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
686354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
686355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
686355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
686356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
686361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
686362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
686440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
686446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
686451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
686548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
686549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
686549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
686550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
686551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
686551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
686551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
686552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
686606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
686607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
686608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
686609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
686609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
686614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
686619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
686733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
686822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
686823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
686824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
686825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
686988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
687111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
687112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
690172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
690177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
690178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
690179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
690180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
690292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
690293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
690294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
690294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
690295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
690398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
693348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
696497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
696502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
696503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
696504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
696505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
696615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
696616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
696617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
696618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
696620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
697751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
697751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.4ns 
697752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
700356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
701210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
701212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 
701212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
701220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
701231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
701233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
701235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
701236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
701250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
701252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
701254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
701257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
701258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
701267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
701268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
701269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
701315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
701316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
701317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
701317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
701318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
701389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
701389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
701390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
701391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
701391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
701395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
701396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
701396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
701397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
701398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
701398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
701485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
701485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
701486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
701487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
701488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
701488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
701575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
701575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
701576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
701576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
701576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
701577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
701578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
701578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
701579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
701579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
701579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
701580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
701580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
701581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
701581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
701581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
701582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
701582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
701583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
701585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
701624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
701625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
701682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
701683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
701684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
701685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
701686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
701686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
701733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
701735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
701736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
701737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
701738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
701739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
701739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
701788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
701790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
701793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
701854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
701915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
701915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
701915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
704534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
705423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
705454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.82ms