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

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

tests
0

failures
0

ignored
11m33.45s

duration
100%

successful

Tests

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

Standard output

300        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
327        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.21ms 
572        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596        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)

1436       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1437       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1441       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1441       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2851       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8282       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.71s 
8367       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8404       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.3ns 
8419       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8420       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.23ms 
8424       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11550      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
11553      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12513      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.28ms 
12529      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12530      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 526.51ns 
12532      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15411      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
15413      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16384      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.43ms 
16388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16388      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.9ns 
16392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19214      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
19215      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20069      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20075      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
20078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20079      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.51ns 
20080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22795      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
22795      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23688      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
23692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23692      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 521.71ns 
23694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26323      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
26324      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27185      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27233      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.87ms 
27242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27242      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.7ns 
27243      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29884      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
29884      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30785      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.57ms 
30787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30791      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.96ms 
30792      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33409      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
33409      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
34261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
34264      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 732.31ns 
34266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34266      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.1ns 
34267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36857      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
36858      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37727      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.41ns 
37729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37730      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.4ns 
37731      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40327      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
40328      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41179      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
41182      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 645.71ns 
41185      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41185      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.3ns 
41186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43818      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
43819      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
44645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
44648      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.31ns 
44651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
44651      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.5ns 
44653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47266      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
47266      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
48177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
48180      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 796.41ns 
48182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
48182      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.8ns 
48183      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50816      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
50816      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
51662      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
51698      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.07ms 
51700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
51700      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.1ns 
51701      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54284      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
54284      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
55133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
55164      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.15ms 
55168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
55169      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.2ms 
55171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57734      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
57735      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
58585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
58748      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 152.66ms 
58752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
58752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.5ns 
58753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61323      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
61324      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
62160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
62164      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
62166      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
62166      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.1ns 
62167      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
64724      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
65581      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
65584      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
65588      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
65588      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.9ns 
65589      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68164      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
68165      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
68979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
69014      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.57ms 
69016      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
69017      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.2ns 
69018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71598      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
71598      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
72415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
72432      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.46ms 
72436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
72436      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.9ns 
72439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
75022      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
75865      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
75878      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.74ms 
75880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
75880      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.3ns 
75881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78440      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
78441      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
79273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
79286      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
79289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
79289      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.81ns 
79290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81854      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
81854      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
82691      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
82712      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.89ms 
82720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
82721      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.63ms 
82723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85271      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
85271      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
86110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
86128      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms 
86129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
86130      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.1ns 
86130      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88667      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
88667      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
89501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
89504      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
89506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
89506      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.5ns 
89507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92082      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
92082      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
92909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
92949      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.07ms 
92950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
92951      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.3ns 
92952      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95531      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
95531      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
96344      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
96387      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.91ms 
96389      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
96389      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns 
96390      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98957      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
98957      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
99792      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
99822      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.3ms 
99826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
99827      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.51ms 
99829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
102385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
103224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
103238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
103243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
103244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 682.81ns 
103246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
105845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
106688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
106700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.13ms 
106702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
106703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.3ns 
106704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
109256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
110092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
110102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
110103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
110103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
110104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
112651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
113488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
113498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.93ms 
113504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
113505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337ns 
113506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
116093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
116905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
116913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
116918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
116918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.4ns 
116919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
119513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
120326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
120333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
120335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
120335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.1ns 
120336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
122911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
123751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
123756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
123758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
123758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.1ns 
123762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
126325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
127158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
127168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.89ms 
127170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
127170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.1ns 
127171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
129745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
130577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
130613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.97ms 
130616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
130617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.4ns 
130618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
133165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
133998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
134017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.52ms 
134019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
134019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.2ns 
134020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
136578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
137423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
137442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.95ms 
137443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
137443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.9ns 
137444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
139992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
140831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
140845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.89ms 
140847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
140847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.4ns 
140848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
143419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
144228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
144241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.66ms 
144243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
144243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
144243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
146813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
147623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
147654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.81ms 
147656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
147656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
147657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
150219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
151048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
151050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
151052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
151052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
151053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
153608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
154441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
154445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
154447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
154448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.2ns 
154449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
156989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
157819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
157826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
157827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
157828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
157828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
160363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
161191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
161199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
161200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
161200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
161201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
163750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
164585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
164601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms 
164603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
164603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
164604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
167172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
167986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
167993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.52ms 
167994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
167994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
167995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
170562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
171377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
171380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
171382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
171382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.4ns 
171383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
173961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
174790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
174793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
174795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
174795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
174796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
177337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
178173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
178177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
178179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
178179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.6ns 
178180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
180717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
181547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
181599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44ms 
181602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
181602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.3ns 
181603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
184141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
184968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
185029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.1ms 
185031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
185031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.6ns 
185032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
187573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
188399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
188403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
188405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
188405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.6ns 
188406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
190965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
191770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
191809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.08ms 
191811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
191812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.4ns 
191813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
194370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
195176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
195202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.26ms 
195204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
195204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
195205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
197767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
198597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
198600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 939.91ns 
198601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
198601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
198603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
201137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
201964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
202072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 96.52ms 
202077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
202078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.6ns 
202079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
204636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
205462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
205470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
205473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
205473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.2ns 
205474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
207995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
208821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
208827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
208828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
208829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.6ns 
208829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
211355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
212185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
212203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.29ms 
212207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
212208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.2ns 
212208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
214758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
215559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
215572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.35ms 
215574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
215574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
215575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
218106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
218908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
218912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
218913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
218913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
218914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
221460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
222291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
222295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
222296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
222296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
222297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
224828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
225655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
225670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.33ms 
225671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
225671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
225672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
228208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
229047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
229059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
229061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
229061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
229062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
231601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
232427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
232439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.74ms 
232444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
232445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.1ns 
232446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
234971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
235798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
235801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 985.81ns 
235804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
235804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.7ns 
235805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
238354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
239182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
239185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
239186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
239186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
239187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
241740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
242545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
242550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
242551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
242551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
242552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
245111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
245916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
245919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 864.71ns 
245920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
245920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
245921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
248492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
249322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
249325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 522.9ns 
249326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
249326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
249327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
251856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
252681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
252685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
252686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
252687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.24ms 
252688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
255221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
256048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
256051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 835.31ns 
256053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
256053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.5ns 
256054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
258581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
259434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
259490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.92ms 
259493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
259493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119ns 
259494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
262024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
262853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
262884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.16ms 
262886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
262886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
262887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
265443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
266244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
266268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.09ms 
266270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
266270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
266271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
268812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
269613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
269648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.19ms 
269649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
269649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.1ns 
269650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
272193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
273020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
273039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.01ms 
273042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
273042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.1ns 
273043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
275565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
276393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
276425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.84ms 
276428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
276428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.6ns 
276429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
278958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
279781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
279798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
279799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
279799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
279800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
282312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
283136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
283149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ms 
283150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
283150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
283151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
285663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
286487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
286502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.06ms 
286503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
286503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
286504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
289074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
289879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
289892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.72ms 
289893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
289893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
289894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
292430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
293232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
293249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.71ms 
293250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
293250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
293251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
295785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
296611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
296627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.99ms 
296628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
296629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.6ns 
296629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
299171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
300005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
300022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.41ms 
300024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
300024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.2ns 
300025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
302554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
303381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
303396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.14ms 
303398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
303398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
303398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
305950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
306772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
306786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.07ms 
306787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
306787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
306788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
309299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
310123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
310138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
310139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
310139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
310140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
312657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
313485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
313500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
313502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
313502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
313502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
316046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
316852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
316858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
316860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
316860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
316861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
319412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
320216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
320228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.26ms 
320230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
320230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
320231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
322779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
323607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
323611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
323613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
323613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.1ns 
323614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
326147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
326977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
326979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.71ns 
326981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
326981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
326981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
329517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
330348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
330350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 739.01ns 
330352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
330352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
330353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
332891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
333720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
333726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
333727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
333727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
333728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
336265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
337094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
337100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.39ms 
337101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
337101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
337102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
339658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
340465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
340476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.97ms 
340477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
340477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
340478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
343037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
343848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
343852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
343853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
343853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
343854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
346421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
347254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
347256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 503.9ns 
347257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
347257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
347258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
349809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
350640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
350645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
350646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
350646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
350647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
353186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
354015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
354017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 604.11ns 
354018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
354019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
354019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
356547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
357377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
357379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 553.9ns 
357381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
357381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
357381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
359916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
360743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
360745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 555ns 
360746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
360746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
360747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
363303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
364109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
364112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
364114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
364114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
364115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
366668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
367475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
367482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.78ms 
367484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
367484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
367484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
370043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
370850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
370887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.61ms 
370889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
370889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
370890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
373426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
374256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
374262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
374263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
374263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
374264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
376805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
377635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
377639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
377640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
377640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
377641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
380186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
381021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
381033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ms 
381035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
381035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
381035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
383565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
384392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
384395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
384396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
384396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
384397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
386930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
387759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
387762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
387763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
387763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
387764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
390324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
391131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
391135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
391136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
391136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
391137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
393696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
394502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
394515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.62ms 
394516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
394516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
394517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
397062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
397902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
397906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 372.41ns 
397908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
397908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
397909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
400434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
401258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
401283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.38ms 
401285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
401285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
401285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
403815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
404643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
404646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
404648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
404648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
404648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
407185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
408013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
408028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.08ms 
408029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
408030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
408030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
410575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
411407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
411421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.48ms 
411423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
411423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
411423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
413992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
414800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
414819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.64ms 
414820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
414820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
414821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
417388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
418197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
418199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 497.2ns 
418201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
418201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
418201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
420763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
421594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
421599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
421600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
421600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
421601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
424148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
424984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
424987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
424989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
424989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.5ns 
424990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
427534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
428368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
428370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.91ns 
428372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
428372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
428372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
430912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
431745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
431747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 753.5ns 
431748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
431748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
431749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
434306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
435120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
435123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
435124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
435124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
435125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
437676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
438509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
438512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
438513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
438513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
438514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
441050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
441890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
441898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ms 
441900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
441900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
441901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
444446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
445278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
445284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
445286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
445286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
445287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
447829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
448642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
448649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.81ms 
448652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
448652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.5ns 
448653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
451216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
452059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
452066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
452067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
452067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.4ns 
452068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
454616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
455465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
455469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
455470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
455470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
455471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
458000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
458841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
458844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
458846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
458846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
458846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
461394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
462212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
462214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 747.21ns 
462215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
462215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
462216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
464771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
465609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
465612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 915.81ns 
465613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
465613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
465614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
468135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
468973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
468975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 798.61ns 
468977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
468977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
468977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
471496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
472337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
472346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.42ms 
472347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
472347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
472348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
474926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
475769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
475773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
475775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
475775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
475775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
478308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
479148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
479153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.29ms 
479154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
479154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
479155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
481674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
482510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
482513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 780.81ns 
482514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
482514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
482515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
485054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
485892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
485894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 553.21ns 
485896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
485896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
485896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
488410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
489245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
489248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
489249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
489249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
489250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
491787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
492601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
492603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 723.91ns 
492604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
492605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
492605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
495137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
495976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
495979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 963.71ns 
495980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
495980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
495980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
498502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
499337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
499339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.01ns 
499340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
499341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
499341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
501879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
502691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
502695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
502696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
502696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
502697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
505229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
506068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
506071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.21ns 
506072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
506072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
506073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
508607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
509421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
509429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.16ms 
509431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
509431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
509431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
511977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
512815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
512817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 524.4ns 
512818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
512818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
512819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
515327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
516169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
516175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
516176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
516176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
516177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
518707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
519542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
519544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 778.81ns 
519545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
519545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
519546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
522068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
522907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
522910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 677.51ns 
522911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
522911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
522912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
525454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
526291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
526295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
526296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
526296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
526297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
528826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
529667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
529669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 818.21ns 
529671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
529671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
529671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
532213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
533051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
533054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
533055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
533055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
533056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
535583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
536420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
536423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
536424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
536424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
536425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
538973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
539814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
539818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
539819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
539819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
539820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
542358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
543202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
543209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
543210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
543210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
543211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
545762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
546602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
546609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.55ms 
546611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
546611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
546611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
549142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
549983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
549988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
549990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
549990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
549991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
552538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
553378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
553384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
553385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
553385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
553386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
555927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
556743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
556752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
556754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
556754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
556755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
559305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
560143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
560153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
560154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
560154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
560155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
562688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
563527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
563536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.77ms 
563537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
563537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
563538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
566053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
566890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
566896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
566898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
566898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
566898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
569433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
570270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
570288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.7ms 
570290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
570290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
570291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
572827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
573645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
573665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.85ms 
573667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
573667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
573667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
576203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
577041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
577059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.71ms 
577060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
577060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
577061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
579598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
580436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
580455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.02ms 
580458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
580458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.8ns 
580459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
582996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
583813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
583831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.84ms 
583833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
583833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
583833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
586366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
587203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
587248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.1ms 
587249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
587249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
587250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
589790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
590630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
590634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
590635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
590635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
590636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
593170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
593987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
593992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
593993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
593993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
593994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
596538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
597378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
597382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
597383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
597383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
597384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
599927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
600768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
600781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.83ms 
600782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
600783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
600783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
603331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
604172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
604178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
604179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
604179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
604180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
606732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
607551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
607554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
607555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
607555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
607556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
610094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
610935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
610944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
610945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
610945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
610946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
613494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
614334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
614344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.88ms 
614345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
614345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
614346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
616891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
617756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
617768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ms 
617770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
617770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
617770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
620318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
621137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
621140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 948.41ns 
621141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
621141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
621142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
623685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
624529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
624532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
624534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
624534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
624534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
627073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
627913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
627919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.78ms 
627920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
627920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
627921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
630457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
631296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
631300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
631302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
631302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
631303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
633841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
634680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
634720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.51ms 
634722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
634722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
634723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
637263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
638104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
638125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.05ms 
638126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
638126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
638127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
640667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
641507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
641517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
641519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
641519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
641519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
644065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
644886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
644888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 270ns 
644890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
644890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
644891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
647431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
648278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
648355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.24ms 
648357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
648357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
648358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
650908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
651750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
651782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.8ms 
651785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
651785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
651785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
654333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
655176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
655178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 200.7ns 
655179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
655179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
655180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
657734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
658578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
658580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 212ns 
658581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
658581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
658582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
661131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
661973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
661975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 217.7ns 
661976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
661976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
661977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
664522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
665363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
665364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 359.6ns 
665366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
665366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
665366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
667904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
668747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
668838     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
668846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 95.91ms 
668849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
668849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250ns 
668851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
671436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
672278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
672324     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
672324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.65ms 
672326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
672326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
672327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
674873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
675715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
675716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 
675742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
675778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
675791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
675795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
675805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
675806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
675808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
675809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
675813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
675814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
675816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
675817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
676030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
676031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
676033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
676034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
676035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
676182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
676183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
676186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
676188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
676190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
676191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
676381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
676382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
676384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
676384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
676385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
676386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
676530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
676532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
676534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
676534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
676535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
676536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
676544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
676545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
676546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
676548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
676549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
676550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
676558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
676559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
676560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
676561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
676561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
676562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
676714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
676715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
676716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
676854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
676855     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)'' 
676856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
676859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
676860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
676860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
676861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
676862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
676866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
676867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
676868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
676870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
676871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
676985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
676989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
676991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
676992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
676993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
676994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
676995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
677119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
677121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
677122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
677123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
677124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
677125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
677126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
677127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
677277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
677279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
677371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
677376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
677381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
677382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
677383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
677384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
677385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
677385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
677386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
677386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
677395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
677401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
677506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
677509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
677510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
677512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
677512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
677513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
677513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
677514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
677570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
677576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
677675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
677676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
677679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
677681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
677682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
677683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
677864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
677868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
677871     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)'' 
677873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
677874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
677878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
677878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
677879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
677888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
677892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
677894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
677895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
677990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
677991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
677992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
677993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
677994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
677995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
678106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
678107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
678109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
678110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
678111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
678112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
678112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
678113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
678203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
678205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
678281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
678282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
678282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
678287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
678290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
678294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
678412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
678413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
678414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
678415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
678425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
678505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
682003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
682004     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)'' 
682007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
682009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
682009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
682010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
682010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
682018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
682019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
682020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
682020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
682021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
682112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
682116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
682116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
682117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
682118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
682118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
682119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
682212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
682212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
682213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
682214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
682215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
682215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
682216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
682216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
682291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
682292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
682371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
682375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
682379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
682380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
682381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
682381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
682392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
682473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
682474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
682475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
682475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
682545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
682554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
682555     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)'' 
682556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
682557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
682558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
682558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
682558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
682570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
682570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
682571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
682572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
682572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
682657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
682657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
682658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
682659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
682660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
682748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
682752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
682753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
682754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
682754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
682755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
682755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
682851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
682851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
682852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
682853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
682854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
682854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
682855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
682855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
682856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
682857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
682857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
682858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
682858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
682859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
682859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
682944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
682945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
682951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
683027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
683105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
683106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
683107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
683108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
683109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
683109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
683110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
683110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
683111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
683195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
683201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
683290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
683291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
683292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
683293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
683293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
683294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
683294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
683295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
683300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
683301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
683379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
683384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
683390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
683532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
683533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
683534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
683535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
683535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
683536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
683536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
683537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
683590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
683591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
683592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
683592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
683593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
683599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
683604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
683716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
683801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
683802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
683803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
683804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
683964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
684049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
684050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
686975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
686979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
686981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
686982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
686982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
687094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
687095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
687096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
687097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
687098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
687200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
689985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
693031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
693035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
693036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
693036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
693037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
693146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
693147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
693148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
693149     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)' ...' 
693149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
694240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
694241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
694242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
696862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
697733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
697735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
697735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
697741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
697751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
697753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
697755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
697756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
697761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
697761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
697765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
697765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
697767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
697776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
697777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
697778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
697823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
697824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
697825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
697825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
697826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
697883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
697883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
697884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
697885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
697886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
697889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
697890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
697890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
697891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
697892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
697892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
697964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
697965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
697966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
697967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
697968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
697969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
698041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
698042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
698042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
698043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
698043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
698044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
698045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
698045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
698046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
698047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
698047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
698048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
698048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
698049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
698049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
698050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
698050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
698051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
698052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
698054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
698084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
698085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
698129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
698130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
698131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
698132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
698133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
698134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
698173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
698175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
698176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
698177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
698179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
698180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
698180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
698220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
698223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
698226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
698274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
698382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
698382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
698383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
700989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
701874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
701889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.24ms