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

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

tests
0

failures
0

ignored
11m30.86s

duration
100%

successful

Tests

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

Standard output

911        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
938        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 14.5ms 
1178       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1202       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)

2077       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2079       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2080       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2080       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3819       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9707       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.53s 
9790       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9828       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.9ns 
9845       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9845       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 715.51ns 
9853       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12932      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
12935      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13988      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.93ms 
13999      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13999      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.2ns 
14001      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16869      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
16870      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
17819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
17846      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ms 
17851      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
17852      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.91ns 
17854      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20662      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
20665      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
21615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
21626      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ms 
21631      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
21633      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.65ms 
21634      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24355      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
24356      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
25215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
25220      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
25228      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
25229      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 577.61ns 
25230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27895      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
27895      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
28729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
28772      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.55ms 
28776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
28776      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 436.61ns 
28778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31414      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
31415      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
32258      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
32278      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.31ms 
32282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
32283      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.71ns 
32284      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34898      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
34898      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
35740      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
35744      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.31ns 
35747      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
35747      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.41ns 
35748      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38374      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
38374      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
39204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
39207      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.71ns 
39210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
39210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.61ns 
39213      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41841      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
41842      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
42686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
42690      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 729.81ns 
42692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
42693      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.31ns 
42694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45304      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
45305      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
46152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
46155      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.01ns 
46158      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
46158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.2ns 
46159      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48794      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
48794      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
49605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
49608      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 786.51ns 
49612      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
49614      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.56ms 
49615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52215      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
52216      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
53063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
53180      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 94.62ms 
53192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
53193      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.47ms 
53195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55797      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
55797      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
56633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
56703      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.8ms 
56712      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
56713      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 640.51ns 
56715      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
59299      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
60115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
60287      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 163.46ms 
60289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
60289      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173ns 
60290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
62850      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
63706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
63713      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
63716      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
63717      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.81ns 
63718      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66279      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
66280      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
67121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
67124      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
67126      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
67126      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.9ns 
67127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69749      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
69750      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
70579      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
70619      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.08ms 
70622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
70622      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.41ns 
70624      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73186      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
73187      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
74015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
74031      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.61ms 
74033      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
74034      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.2ns 
74035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76608      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
76608      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
77428      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
77444      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.34ms 
77449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
77449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 509.01ns 
77454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80031      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
80032      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
80862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
80878      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms 
80881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
80881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.11ns 
80882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83433      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
83434      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
84265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
84280      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.84ms 
84282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
84283      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.9ns 
84284      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86861      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
86861      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
87671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
87698      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.48ms 
87700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
87700      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.5ns 
87701      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90264      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
90265      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
91090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
91093      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
91095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
91096      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.3ns 
91097      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
93652      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
94476      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
94517      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.52ms 
94519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
94520      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.31ns 
94521      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97082      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
97082      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
97885      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
97944      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.43ms 
97953      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
97953      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 580.21ns 
97955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
100513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
101341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
101385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.87ms 
101387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
101387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.5ns 
101388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
103906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
104733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
104740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.47ms 
104742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
104742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.4ns 
104743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
107288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
108116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
108133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms 
108139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
108139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.7ns 
108140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
110688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
111513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
111524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.11ms 
111526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
111526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
111527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
114057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
114889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
114896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.46ms 
114898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
114898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.6ns 
114899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
117468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
118298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
118306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
118309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
118309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.91ns 
118310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
120853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
121677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
121684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
121686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
121686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.3ns 
121687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
124226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
125021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
125025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
125027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
125027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.3ns 
125028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
127556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
128374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
128384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.25ms 
128386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
128386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
128387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
130907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
131728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
131780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.2ms 
131783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
131793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.14ms 
131795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
134375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
135173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
135190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.03ms 
135196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
135196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.11ns 
135197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
137742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
138565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
138583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.93ms 
138585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
138585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.8ns 
138586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
141098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
141921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
141938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.52ms 
141940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
141940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.1ns 
141941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
144482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
145278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
145295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.8ms 
145297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
145297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
145298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
147817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
148641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
148680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.48ms 
148682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
148682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
148683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
151206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
152031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
152033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
152035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
152035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
152036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
154574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
155392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
155397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
155398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
155399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.3ns 
155399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
157913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
158734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
158742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.25ms 
158744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
158744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.8ns 
158745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
161262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
162081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
162089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.16ms 
162091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
162092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 690.41ns 
162092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
164623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
165441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
165474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.57ms 
165478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
165483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.15ms 
165485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
168002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
168821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
168834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.86ms 
168836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
168836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
168837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
171370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
172180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
172184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
172186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
172186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.2ns 
172187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
174738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
175556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
175560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
175562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
175562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.1ns 
175562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
178066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
178883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
178888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
178889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
178889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
178890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
181410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
182203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
182291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.6ms 
182293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
182293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.3ns 
182294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
184813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
185626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
185710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.97ms 
185711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
185712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.8ns 
185712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
188206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
189025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
189029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
189030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
189030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
189031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
191532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
192328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
192400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.64ms 
192404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
192405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.51ns 
192406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
194905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
195722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
195752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.31ms 
195754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
195754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
195754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
198262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
199077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
199080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
199081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
199081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
199083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
201600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
202418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
202570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 139.53ms 
202572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
202572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
202573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
205092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
205911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
205923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
205924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
205924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
205925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
208445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
209239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
209247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.46ms 
209248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
209248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
209249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
211760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
212594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
212611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.02ms 
212613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
212613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
212614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
215119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
215932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
215945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.94ms 
215947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
215947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
215948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
218451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
219248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
219252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
219253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
219253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
219254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
221772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
222590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
222595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
222596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
222596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
222597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
225090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
225904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
225927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.38ms 
225929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
225929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
225930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
228453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
229250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
229268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.11ms 
229269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
229269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
229270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
231796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
232616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
232632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.45ms 
232633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
232634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
232634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
235153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
235979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
235983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
235984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
235984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
235985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
238522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
239345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
239349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
239351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
239351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
239352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
241860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
242692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
242699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
242701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
242701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.2ns 
242702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
245206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
246024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
246028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
246029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
246029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
246030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
248553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
249374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
249376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 697.61ns 
249378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
249379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.5ns 
249380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
251878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
252693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
252697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
252698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
252698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
252699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
255215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
256012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
256015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
256016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
256016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
256017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
258537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
259357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
259410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.5ms 
259412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
259412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.1ns 
259413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
261942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
262761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
262801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.03ms 
262803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
262803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
262804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
265318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
266114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
266147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.41ms 
266148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
266148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
266149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
268693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
269513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
269558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.66ms 
269559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
269559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
269560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
272077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
272905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
272941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.3ms 
272944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
272944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.7ns 
272945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
275489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
276285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
276382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.94ms 
276385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
276385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.8ns 
276386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
278902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
279720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
279749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.75ms 
279751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
279751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
279751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
282252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
283072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
283094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.07ms 
283095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
283095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
283096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
285621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
286437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
286463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.29ms 
286464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
286464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
286465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
288976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
289794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
289815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.05ms 
289816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
289816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
289817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
292328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
293120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
293149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.88ms 
293151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
293151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
293152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
295677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
296498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
296528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.47ms 
296530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
296530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265ns 
296531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
299035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
299855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
299881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23ms 
299883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
299883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
299884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
302398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
303190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
303216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.05ms 
303218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
303218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
303219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
305731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
306551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
306576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.88ms 
306579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
306579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
306580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
309090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
309907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
309934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.02ms 
309936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
309936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
309936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
312454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
313272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
313299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.51ms 
313300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
313300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
313301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
315804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
316621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
316629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
316631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
316631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
316632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
319125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
319944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
319963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.21ms 
319964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
319964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
319965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
322486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
323304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
323308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
323309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
323310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
323310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
325813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
326626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
326630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
326631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
326631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
326632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
329159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
329956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
329958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.61ns 
329959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
329959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
329960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
332481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
333301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
333308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
333310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
333310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
333313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
335842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
336665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
336672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
336674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
336674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.4ns 
336675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
339188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
339987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
340000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.29ms 
340001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
340001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
340002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
342543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
343360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
343364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
343365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
343365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
343366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
345864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
346687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
346689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.11ns 
346691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
346691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
346691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
349194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
349987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
349993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
349994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
349994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
349995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
352510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
353332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
353334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.71ns 
353335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
353335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
353336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
355846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
356664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
356667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 634.81ns 
356668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
356668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
356669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
359185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
359981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
359983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 677.81ns 
359985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
359985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
359986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
362512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
363336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
363340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
363342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
363342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
363342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
365856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
366678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
366687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
366688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
366688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
366689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
369211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
370034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
370038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
370040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
370040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
370040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
372556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
373379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
373387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.35ms 
373388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
373388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
373389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
375919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
376714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
376719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
376720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
376720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
376721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
379238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
380053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
380069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.03ms 
380071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
380071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
380072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
382580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
383401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
383405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
383406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
383406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
383407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
385947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
386794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
386798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
386799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
386799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
386800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
389313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
390130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
390134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
390135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
390135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
390136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
392645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
393441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
393458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.05ms 
393460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
393460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
393460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
395968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
396783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
396787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 552.71ns 
396789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
396789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
396790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
399298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
400091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
400130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.33ms 
400132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
400132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
400133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
402643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
403458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
403461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
403463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
403463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
403463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
405969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
406788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
406810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20ms 
406812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
406812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
406813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
409344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
410162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
410185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.39ms 
410187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
410187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
410188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
412719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
413544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
413569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.09ms 
413571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
413571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
413572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
416104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
416926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
416928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 567.31ns 
416930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
416930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
416931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
419463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
420260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
420266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
420268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
420268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
420269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
422797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
423614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
423618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
423619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
423619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
423620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
426134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
426931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
426933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 884.31ns 
426934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
426935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
426935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
429451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
430268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
430271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 901.01ns 
430272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
430272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
430273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
432793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
433614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
433618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
433619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
433619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
433620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
436118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
436941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
436944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
436947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
436948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.2ns 
436949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
439463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
440287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
440296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ms 
440298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
440298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
440299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
442793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
443621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
443633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.11ms 
443637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
443637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.7ns 
443638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
446150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
446973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
446986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
446989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
446989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
446990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
449508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
450335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
450354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.19ms 
450355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
450355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
450356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
452879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
453710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
453715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
453717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
453717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.2ns 
453718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
456235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
457066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
457073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 
457074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
457074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
457075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
459590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
460424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
460426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 750.51ns 
460428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
460428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
460428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
462934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
463771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
463774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
463775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
463775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
463776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
466291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
467118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
467120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 891.61ns 
467121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
467121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
467122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
469635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
470465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
470476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.01ms 
470478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
470478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
470479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
472993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
473824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
473828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
473829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
473829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
473830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
476351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
477179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
477186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
477187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
477187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
477188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
479699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
480529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
480531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 793.41ns 
480533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
480533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
480534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
483063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
483896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
483898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717.21ns 
483900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
483900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
483901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
486422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
487258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
487262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
487263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
487263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
487264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
489791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
490617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
490620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
490621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
490621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
490622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
493143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
493971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
493974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
493976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
493976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
493976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
496499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
497332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
497335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
497337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
497337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.6ns 
497338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
499857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
500661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
500666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
500667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
500667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
500668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
503185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
504016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
504019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
504021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
504021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
504022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
506539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
507375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
507386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.64ms 
507387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
507387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
507388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
509898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
510724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
510727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
510728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
510728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
510729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
513243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
514071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
514078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.43ms 
514079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
514080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
514080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
516598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
517424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
517427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 937.01ns 
517428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
517428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
517429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
519954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
520785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
520788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 782.91ns 
520789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
520789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
520790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
523310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
524137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
524142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
524144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
524144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
524144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
526652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
527459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
527462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
527464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
527465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.5ns 
527465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
529959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
530784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
530787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
530788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
530788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
530789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
533292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
534122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
534125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
534128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
534128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
534129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
536645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
537470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
537474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
537476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
537476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
537477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
539990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
540821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
540836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.93ms 
540837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
540837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
540838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
543364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
544192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
544208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.04ms 
544210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
544210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
544210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
546735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
547561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
547572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
547573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
547574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
547574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
550099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
550929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
550940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.18ms 
550942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
550942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
550942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
553443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
554270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
554297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.13ms 
554298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
554298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
554299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
556808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
557635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
557661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.85ms 
557662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
557662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
557663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
560178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
561009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
561034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.4ms 
561035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
561035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
561036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
563587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
564424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
564438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.49ms 
564440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
564440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
564440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
566942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
567769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
567800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.44ms 
567801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
567801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
567802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
570310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
571137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
571186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.93ms 
571188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
571188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
571189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
573704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
574530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
574569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.85ms 
574570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
574571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
574571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
577083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
577914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
577957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.67ms 
577959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
577959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
577960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
580474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
581307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
581353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.57ms 
581354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
581354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
581355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
583868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
584699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
584854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 148.75ms 
584856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
584856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
584857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
587366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
588196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
588204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.1ms 
588206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
588206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
588206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
590722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
591548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
591558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.65ms 
591559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
591559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
591560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
594072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
594896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
594902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
594903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
594903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
594904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
597414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
598244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
598263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.64ms 
598264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
598264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
598265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
600807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
601642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
601654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.21ms 
601655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
601655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
601656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
604177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
605006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
605009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
605010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
605011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
605011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
607533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
608362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
608380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.5ms 
608382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
608382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
608382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
610896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
611722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
611739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.46ms 
611740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
611740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
611741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
614288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
615124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
615145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.14ms 
615147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
615147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.7ns 
615148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
617672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
618504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
618507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
618509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
618509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
618509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
621008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
621842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
621845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
621847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
621847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
621847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
624377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
625200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
625207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
625208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
625208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
625209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
627719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
628544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
628551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
628552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
628552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
628553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
631048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
631874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
631983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 104.04ms 
631985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
631985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.9ns 
631986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
634492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
635322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
635350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.31ms 
635351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
635351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
635352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
637868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
638699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
638722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.72ms 
638724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
638724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
638724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
641249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
642079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
642081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 296.61ns 
642084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
642084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.3ns 
642085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
644620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
645448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
645659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 200.33ms 
645661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
645662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.3ns 
645663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
648230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
649063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
649116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.29ms 
649118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
649118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
649118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
651631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
652459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
652461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 375.11ns 
652463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
652463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
652463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
654994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
655821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
655823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 365.11ns 
655825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
655825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
655825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
658332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
659164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
659166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 367.31ns 
659171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
659171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.2ns 
659172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
661705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
662532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
662534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.51ns 
662536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
662536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
662537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
665039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
665887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
665996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.03ms 
665999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
665999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.4ns 
666000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
668536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
669365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
669416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.14ms 
669417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
669417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
669419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
671956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
672793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
672795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
672825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
672871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
672895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
672904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
672917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
672921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
672923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
672926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
672929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
672932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
672937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
672938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
673195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
673197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
673199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
673200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
673201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
673337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
673339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
673342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
673345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
673346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
673347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
673516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
673518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
673520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
673521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
673521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
673525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
673672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
673674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
673675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
673676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
673677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
673678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
673688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
673689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
673690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
673693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
673694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
673696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
673706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
673707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
673708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
673712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
673713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
673714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
673862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
673863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
673865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
673979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
673981     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)'' 
673983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
673985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
673986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
673988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
673989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
673992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
673995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
673997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
673998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
673999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
674000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
674104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
674108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
674110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
674110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
674111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
674112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
674114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
674239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
674240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
674241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
674243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
674244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
674244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
674246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
674248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
674347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
674349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
674440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
674444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
674450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
674452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
674453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
674455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
674458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
674458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
674459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
674460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
674470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
674475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
674578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
674580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
674582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
674583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
674584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
674585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
674585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
674588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
674644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
674649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
674740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
674742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
674744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
674746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
674747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
674748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
674895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
674901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
674904     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)'' 
674906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
674908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
674909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
674910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
674911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
674922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
674928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
674930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
674931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
675083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
675085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
675086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
675087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
675088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
675090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
675196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
675198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
675199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
675201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
675201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
675202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
675202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
675204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
675284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
675285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
675358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
675359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
675360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
675364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
675368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
675372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
675493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
675496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
675497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
675498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
675508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
675592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
679244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
679245     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)'' 
679251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
679252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
679253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
679254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
679255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
679263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
679264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
679266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
679266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
679267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
679361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
679365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
679367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
679368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
679368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
679369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
679370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
679466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
679468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
679469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
679470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
679471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
679471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
679472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
679473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
679550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
679552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
679627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
679631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
679635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
679636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
679637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
679638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
679648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
679728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
679730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
679730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
679731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
679804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
679814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
679814     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)'' 
679816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
679817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
679818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
679818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
679818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
679829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
679831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
679832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
679832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
679833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
679921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
679923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
679924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
679924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
679925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
680017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
680022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
680023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
680024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
680024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
680025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
680025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
680125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
680127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
680128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
680129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
680129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
680130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
680130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
680131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
680132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
680133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
680134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
680134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
680135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
680135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
680136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
680224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
680226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
680232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
680311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
680392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
680394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
680394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
680395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
680396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
680396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
680397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
680397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
680398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
680484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
680490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
680624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
680625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
680625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
680626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
680627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
680627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
680627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
680628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
680633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
680634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
680713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
680718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
680724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
680823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
680824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
680824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
680825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
680826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
680826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
680826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
680827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
680882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
680884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
680884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
680885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
680886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
680891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
680897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
681015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
681104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
681105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
681106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
681107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
681275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
681364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
681365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
685085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
685090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
685092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
685093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
685094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
685208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
685210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
685211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
685211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
685212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
685318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
688386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
691702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
691707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
691708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
691709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
691709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
691825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
691826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
691827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
691828     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)' ...' 
691830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
692964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
692965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
692965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
695609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
696467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
696470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
696471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
696478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
696489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
696492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
696494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
696495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
696500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
696502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
696506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
696508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
696509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
696518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
696520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
696522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
696570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
696572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
696572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
696573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
696574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
696646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
696646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
696648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
696649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
696649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
696654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
696654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
696655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
696656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
696658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
696658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
696749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
696750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
696751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
696752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
696753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
696754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
696844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
696845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
696845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
696846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
696847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
696848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
696848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
696849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
696850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
696850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
696851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
696851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
696852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
696852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
696853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
696854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
696854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
696855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
696856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
696859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
696893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
696894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
696949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
696950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
696952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
696953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
696954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
696954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
697004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
697007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
697008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
697010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
697011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
697012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
697012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
697059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
697062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
697065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
697176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
697230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
697230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.6ns 
697231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
699810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
700691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
700724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.38ms