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

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

tests
0

failures
0

ignored
11m28.33s

duration
100%

successful

Tests

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

Standard output

376        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
397        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.99ms 
600        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612        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)

1565       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1568       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1572       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1573       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2972       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8618       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.02s 
8681       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8715       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.1ns 
8732       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8735       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.88ms 
8740       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
11667      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12662      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12687      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.98ms 
12696      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12696      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.4ns 
12697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15546      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
15546      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16543      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.64ms 
16546      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16547      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.81ns 
16548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19284      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
19285      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20229      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
20232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20232      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.9ns 
20233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22957      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
22958      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23822      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.53ms 
23828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23830      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.19ms 
23831      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26456      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
26458      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27303      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.81ms 
27345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27346      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.4ns 
27346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29918      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
29918      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30778      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.85ms 
30780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.7ns 
30781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33356      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
33356      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
34205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
34208      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 806.21ns 
34210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 
34211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36822      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
36823      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37680      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37683      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.31ns 
37686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37686      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.9ns 
37687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40241      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
40242      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41079      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
41082      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 677.01ns 
41085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41085      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.7ns 
41087      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43618      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
43619      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
44458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
44461      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 681.71ns 
44464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
44464      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.2ns 
44465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47024      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
47025      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
47835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
47838      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 598.41ns 
47841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
47841      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.11ns 
47842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50394      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
50394      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
51225      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
51277      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.97ms 
51287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
51287      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 557.21ns 
51292      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53862      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
53862      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
54699      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
54772      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.81ms 
54775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
54775      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.8ns 
54776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57361      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
57362      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
58203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
58390      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 177.71ms 
58393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
58394      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.81ns 
58395      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60959      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
60960      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
61794      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
61799      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
61802      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
61802      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.6ns 
61803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64333      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
64334      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
65174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
65178      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
65182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
65183      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.01ns 
65184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67725      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
67726      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
68562      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
68620      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.53ms 
68624      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
68624      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.7ns 
68625      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71189      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
71190      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
71991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
72007      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 
72008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
72008      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.8ns 
72009      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74538      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
74538      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
75373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
75390      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 
75393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
75394      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 810.81ns 
75399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77956      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
77957      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
78782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
78798      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.17ms 
78800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
78800      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123ns 
78801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81348      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
81348      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
82217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
82233      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.06ms 
82235      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
82237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.46ms 
82238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84803      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
84803      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
85602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
85628      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.76ms 
85629      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
85630      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.2ns 
85631      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88165      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
88165      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
88986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
88989      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
88991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
88991      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
88992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
91498      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
92324      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
92384      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.52ms 
92387      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
92388      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.5ns 
92389      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94932      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
94933      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
95732      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
95788      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.72ms 
95789      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
95790      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns 
95791      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98310      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
98311      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
99136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
99179      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.58ms 
99180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
99181      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.7ns 
99181      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
101687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
102508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
102515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.49ms 
102517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
102517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.2ns 
102518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
105023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
105848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
105860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.06ms 
105862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
105862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
105863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
108398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
109198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
109209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
109211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
109211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.4ns 
109212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
111772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
112601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
112609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.43ms 
112611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
112611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.5ns 
112612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
115176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
116006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
116014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.09ms 
116017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
116018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 528.81ns 
116019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
118584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
119388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
119395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
119398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
119398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.9ns 
119399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
121958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
122783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
122786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
122788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
122788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.8ns 
122789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
125312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
126135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
126145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.71ms 
126147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
126147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.3ns 
126148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
128680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
129509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
129560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.83ms 
129562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
129562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.2ns 
129563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
132099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
132895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
132913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
132915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
132915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.6ns 
132916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
135450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
136279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
136297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.93ms 
136299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
136300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.7ns 
136301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
138803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
139620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
139643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.87ms 
139646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
139646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.5ns 
139648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
142161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
142984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
143001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.19ms 
143002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
143003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.5ns 
143003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
145535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
146356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
146397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.05ms 
146400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
146400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.1ns 
146401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
148903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
149726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
149731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
149735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
149735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.5ns 
149737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
152246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
153062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
153067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
153068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
153068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.2ns 
153069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
155585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
156378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
156387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.35ms 
156389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
156389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.5ns 
156390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
158906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
159722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
159731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.29ms 
159732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
159732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
159733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
162232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
163053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
163071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.94ms 
163073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
163073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.6ns 
163074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
165573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
166389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
166397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.96ms 
166398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
166399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
166399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
168902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
169694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
169698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
169700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
169700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.8ns 
169701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
172214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
173033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
173038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
173039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
173039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
173040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
175546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
176372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
176378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
176381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
176381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
176382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
178923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
179728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
179807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.95ms 
179809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
179809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
179810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
182336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
183156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
183240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.52ms 
183242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
183242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.6ns 
183243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
185754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
186573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
186576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
186577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
186578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
186578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
189070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
189898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
189955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.18ms 
189959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
189964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.12ms 
189965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
192506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
193303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
193334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.02ms 
193335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
193335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
193336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
195870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
196686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
196689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
196707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
196708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.61ns 
196709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
199247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
200108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
200257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 136.97ms 
200259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
200260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 714.41ns 
200261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
202822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
203615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
203627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.81ms 
203628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
203628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
203629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
206152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
206969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
206990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.38ms 
206993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
206994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.8ns 
206995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
209478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
210294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
210311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.34ms 
210312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
210312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
210313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
212799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
213637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
213651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.35ms 
213654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
213655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 867.21ns 
213656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
216167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
216966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
216970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
216972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
216972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135ns 
216972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
219480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
220297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
220302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
220303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
220303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
220304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
222818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
223646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
223671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.27ms 
223672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
223672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
223673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
226239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
227043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
227060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.17ms 
227062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
227062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
227063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
229614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
230439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
230456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.29ms 
230457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
230457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
230458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
232987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
233815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
233819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
233820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
233820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
233821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
236348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
237174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
237178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
237180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
237180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
237181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
239714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
240514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
240519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
240521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
240521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
240522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
243063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
243893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
243897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
243899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
243899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260ns 
243900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
246414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
247236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
247239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 832.51ns 
247240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
247240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
247241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
249747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
250594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
250598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
250600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
250600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
250601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
253148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
253975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
253978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
253980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
253980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
253981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
256469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
257295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
257365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.69ms 
257368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
257368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
257369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
259868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
260684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
260721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.93ms 
260723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
260723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
260724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
263238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
264037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
264067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.86ms 
264069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
264070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233ns 
264071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
266583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
267410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
267459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.79ms 
267461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
267461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
267462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
269970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
270791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
270822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.75ms 
270823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
270823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
270824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
273326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
274153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
274206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.18ms 
274207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
274208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.7ns 
274208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
276751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
277570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
277598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.49ms 
277600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
277600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
277601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
280098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
280916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
280937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.36ms 
280938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
280938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
280939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
283422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
284240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
284264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.26ms 
284266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
284266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
284267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
286771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
287566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
287586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.98ms 
287587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
287588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
287588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
290094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
290914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
290942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.65ms 
290943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
290943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
290944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
293432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
294251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
294277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.23ms 
294278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
294278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
294279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
296766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
297586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
297612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.31ms 
297613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
297613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
297614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
300136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
300954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
300979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.85ms 
300980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
300981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
300981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
303471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
304286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
304307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.23ms 
304309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
304309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
304309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
306799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
307628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
307657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.98ms 
307658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
307658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
307659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
310188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
310986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
311011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.56ms 
311012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
311013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
311013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
313522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
314340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
314348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.83ms 
314349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
314349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
314350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
316834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
317655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
317673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.13ms 
317675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
317675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
317676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
320164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
320987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
320991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
320993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
320993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
320993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
323518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
324337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
324339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 758.61ns 
324341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
324341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
324341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
326835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
327653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
327656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 801.41ns 
327657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
327657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
327658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
330141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
330962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
330970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.99ms 
330971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
330971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
330972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
333488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
334287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
334293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 
334295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
334295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
334295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
336802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
337638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
337651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
337652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
337652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
337653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
340140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
340958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
340962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
340963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
340963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
340964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
343444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
344265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
344267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.81ns 
344268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
344268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
344269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
346779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
347574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
347580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
347581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
347581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
347582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
350090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
350912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
350914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 706.31ns 
350916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
350916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
350916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
353427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
354251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
354254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.21ns 
354255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
354255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
354256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
356777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
357573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
357575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 668.51ns 
357576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
357576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
357577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
360089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
360910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
360914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
360916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
360916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
360917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
363416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
364239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
364248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.27ms 
364250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
364250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
364251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
366772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
367590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
367595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
367596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
367596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
367597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
370118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
370917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
370925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
370926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
370926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
370927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
373448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
374268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
374275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.55ms 
374280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
374280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.7ns 
374283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
376814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
377637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
377654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms 
377655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
377655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
377656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
380174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
380996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
380999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
381001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
381001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
381002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
383532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
384352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
384355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
384357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
384357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
384357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
386863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
387683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
387688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
387689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
387689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
387690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
390168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
390983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
391000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.55ms 
391002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
391002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
391003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
393507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
394322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
394327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 603.21ns 
394329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
394329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
394330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
396808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
397617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
397656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.1ms 
397657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
397658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
397658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
400137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
400953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
400956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
400958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
400958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
400958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
403456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
404272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
404294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.9ms 
404295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
404295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
404296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
406777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
407592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
407615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.13ms 
407617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
407617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
407618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
410128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
410922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
410946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21ms 
410948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
410948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
410949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
413452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
414273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
414276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.41ns 
414277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
414277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
414278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
416769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
417586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
417592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.01ms 
417594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
417594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
417594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
420117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
420936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
420940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
420942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
420942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.5ns 
420943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
423444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
424263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
424266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 860.51ns 
424268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
424268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
424269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
426771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
427568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
427571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 944.11ns 
427572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
427572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
427573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
430075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
430906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
430910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
430911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
430911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
430912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
433416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
434216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
434219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
434221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
434221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
434222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
436729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
437556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
437566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ms 
437568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
437568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
437568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
440054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
440877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
440897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.47ms 
440908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
440909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 792.21ns 
440910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
443452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
444280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
444298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.42ms 
444301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
444301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
444302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
446791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
447623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
447640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.55ms 
447643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
447643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234ns 
447644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
450143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
450972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
450977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
450979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
450979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.8ns 
450980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
453480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
454314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
454320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
454322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
454322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
454322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
456832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
457661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
457663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.81ns 
457665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
457665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
457666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
460142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
460969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
460973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
460974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
460974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
460975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
463470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
464299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
464301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
464303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
464303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
464303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
466809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
467613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
467625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.95ms 
467626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
467626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
467627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
470135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
470966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
470971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
470973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
470973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
470974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
473482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
474311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
474318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
474320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
474320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
474320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
476804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
477631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
477634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 872.51ns 
477635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
477635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
477636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
480134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
480960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
480962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 697.61ns 
480964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
480964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
480964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
483465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
484270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
484274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
484276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
484276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
484276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
486776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
487605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
487608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
487610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
487610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
487611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
490126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
490962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
490966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
490967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
490967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
490968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
493450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
494278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
494281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
494282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
494282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
494283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
496786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
497612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
497618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
497619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
497619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
497620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
500115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
500946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
500949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
500950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
500950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
500951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
503436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
504265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
504276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ms 
504278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
504279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.5ns 
504279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
506799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
507633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
507635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 781.31ns 
507637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
507637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
507639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
510166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
510998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
511006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
511007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
511007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
511008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
513531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
514338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
514341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 948.11ns 
514342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
514342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
514343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
516855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
517684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
517686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 815.81ns 
517687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
517688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
517688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
520194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
521025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
521030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
521032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
521032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
521033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
523549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
524382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
524386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
524387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
524387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
524388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
526925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
527762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
527766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
527767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
527767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
527768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
530273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
531100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
531104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
531105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
531105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
531106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
533596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
534421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
534426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
534427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
534427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
534428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
536925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
537749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
537763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.32ms 
537765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
537765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
537765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
540252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
541080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
541095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 
541097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
541097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
541097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
543589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
544416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
544426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.68ms 
544428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
544428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
544429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
546927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
547732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
547742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ms 
547743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
547744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
547744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
550261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
551088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
551113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.99ms 
551115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
551115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
551116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
553615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
554442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
554467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.49ms 
554468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
554468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
554469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
556955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
557780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
557804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.71ms 
557805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
557805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
557806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
560294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
561123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
561140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.05ms 
561141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
561141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
561142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
563648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
564477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
564508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.61ms 
564510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
564510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
564511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
567006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
567838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
567885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.6ms 
567887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
567887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
567888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
570389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
571220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
571258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.6ms 
571259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
571259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
571260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
573762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
574594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
574636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.82ms 
574637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
574637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
574638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
577137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
577966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
578011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.64ms 
578012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
578012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
578013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
580521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
581351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
581470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.73ms 
581471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
581471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
581472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
583974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
584804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
584815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ms 
584817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
584817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.9ns 
584818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
587317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
588148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
588156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.13ms 
588158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
588158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
588158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
590649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
591477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
591482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
591483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
591483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
591484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
593972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
594799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
594817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.35ms 
594819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
594819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
594819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
597310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
598138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
598149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.88ms 
598150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
598151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.2ns 
598151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
600649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
601479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
601483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
601484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
601484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
601485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
604004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
604810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
604827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.55ms 
604828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
604828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
604829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
607351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
608180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
608197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.23ms 
608198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
608198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
608199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
610688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
611516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
611536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.69ms 
611537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
611537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
611538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
614034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
614863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
614866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
614867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
614867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
614867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
617360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
618191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
618195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
618196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
618196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
618197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
620685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
621514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
621521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.95ms 
621522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
621522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
621523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
624020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
624847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
624854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
624855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
624855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
624856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
627362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
628191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
628258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.41ms 
628260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
628260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
628261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
630859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
631691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
631718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.4ms 
631719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
631719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
631720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
634219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
635051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
635073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.72ms 
635075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
635075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
635076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
637589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
638424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
638427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 308.81ns 
638428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
638428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
638429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
640943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
641771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
641967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 184.57ms 
641969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
641970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220ns 
641971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
644473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
645305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
645356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.4ms 
645357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
645358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
645358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
647845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
648674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
648676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 331.5ns 
648677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
648678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
648678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
651182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
652008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
652010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 382.9ns 
652012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
652012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
652013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
654512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
655341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
655343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 410.31ns 
655344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
655344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
655345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
657829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
658659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
658661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 520.91ns 
658663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
658663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
658663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
661171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
661995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
662081     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
662098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.48ms 
662101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
662102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.6ns 
662103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
664623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
665454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
665505     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
665506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.13ms 
665507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
665507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
665509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
668068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
668900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
668902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ns 
668929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
668972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
668995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
669002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
669009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
669013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
669014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
669017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
669021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
669023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
669027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
669029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
669267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
669269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
669270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
669272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
669273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
669417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
669418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
669421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
669424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
669425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
669428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
669600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
669603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
669604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
669605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
669608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
669610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
669749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
669751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
669753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
669754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
669755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
669756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
669764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
669765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
669766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
669769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
669771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
669772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
669781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
669786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
669787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
669788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
669789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
669790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
669932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
669934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
669936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
670066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
670068     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)'' 
670071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
670072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
670074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
670075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
670077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
670079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
670084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
670085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
670086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
670087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
670088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
670206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
670211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
670213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
670214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
670215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
670216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
670218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
670353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
670355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
670356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
670358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
670359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
670360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
670361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
670362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
670470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
670472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
670633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
670641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
670651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
670652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
670655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
670657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
670658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
670658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
670659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
670660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
670676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
670684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
670795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
670797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
670799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
670801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
670801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
670802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
670803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
670804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
670888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
670895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
671019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
671021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
671024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
671026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
671027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
671029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
671165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
671170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
671173     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)'' 
671175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
671176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
671177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
671178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
671179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
671188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
671194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
671195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
671196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
671292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
671293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
671294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
671296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
671296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
671298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
671400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
671402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
671403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
671405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
671406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
671406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
671407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
671408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
671495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
671496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
671587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
671587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
671588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
671593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
671598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
671602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
671729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
671730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
671731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
671732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
671743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
671866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
675478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
675480     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)'' 
675485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
675487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
675488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
675489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
675491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
675499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
675500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
675502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
675502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
675503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
675603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
675608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
675610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
675611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
675612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
675614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
675615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
675714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
675716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
675717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
675720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
675720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
675721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
675721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
675722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
675848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
675849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
675925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
675929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
675933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
675934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
675935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
675936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
675946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
676043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
676044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
676044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
676045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
676120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
676130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
676131     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)'' 
676132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
676133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
676134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
676134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
676135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
676146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
676147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
676148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
676149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
676149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
676240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
676241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
676242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
676243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
676244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
676337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
676342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
676343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
676343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
676344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
676345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
676345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
676446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
676448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
676448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
676450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
676450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
676451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
676451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
676452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
676453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
676453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
676454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
676455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
676455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
676455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
676456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
676546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
676547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
676554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
676633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
676716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
676717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
676718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
676719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
676720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
676720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
676720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
676721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
676722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
676810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
676816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
676908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
676909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
676910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
676911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
676911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
676912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
676912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
676913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
676918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
676919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
677001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
677007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
677012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
677115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
677116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
677117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
677118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
677118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
677118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
677119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
677119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
677176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
677177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
677178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
677178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
677179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
677185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
677191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
677311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
677402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
677404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
677404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
677405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
677620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
677710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
677710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
680839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
680844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
680845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
680845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
680846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
681019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
681021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
681022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
681023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
681023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
681136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
684207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
687461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
687466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
687467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
687468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
687468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
687585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
687586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
687587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
687588     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)' ...' 
687590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
688780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
688780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
688781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
691402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
692294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
692296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
692296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
692328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
692349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
692360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
692363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
692364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
692369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
692371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
692382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
692385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
692386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
692398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
692400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
692401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
692459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
692468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
692469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
692470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
692471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
692584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
692585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
692587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
692588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
692588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
692592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
692593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
692598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
692599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
692600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
692601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
692753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
692754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
692755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
692756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
692757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
692758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
692897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
692908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
692908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
692909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
692910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
692911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
692912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
692912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
692913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
692914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
692914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
692935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
692936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
692936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
692936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
692937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
692937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
692938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
692953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
692955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
693025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
693027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
693078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
693080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
693082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
693083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
693084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
693085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
693146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
693157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
693159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
693168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
693170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
693171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
693171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
693267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
693269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
693284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
693369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
693445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
693446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.4ns 
693447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
696195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
697048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
697081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.75ms