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

198

tests

0

failures

0

ignored

13m11.81s

duration

100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.817s passed
powPositiveConcrete data()[101] 3.724s passed
powGeq1Concrete data()[102] 3.747s passed
pow2InIntLower data()[103] 3.853s passed
pow2InIntUpper data()[104] 3.830s passed
logSelfConcrete data()[105] 3.768s passed
log1Concrete data()[106] 3.738s passed
logProduct data()[107] 3.726s passed
logTimesBaseConcrete data()[108] 3.781s passed
logProdIdentity data()[109] 3.954s passed
moduloByteIsInByte data()[10] 4.374s passed
logProdIdentityConcrete data()[110] 3.898s passed
logPowIdentity data()[111] 3.895s passed
logPowIdentityConcrete data()[112] 3.719s passed
logPositive data()[113] 3.818s passed
logPositiveConcrete data()[114] 3.788s passed
logMono data()[115] 3.815s passed
logMonoConcrete data()[116] 3.720s passed
powLogLess data()[117] 3.789s passed
powLogMore2 data()[118] 3.832s passed
logLessThanPow data()[119] 3.962s passed
moduloCharIsInChar data()[11] 3.994s passed
logLessThanPowConcrete data()[120] 3.785s passed
logSqueeze data()[121] 3.806s passed
ifthenelse_equals data()[122] 3.796s passed
ifthenelse_equals_1 data()[123] 3.709s passed
ifthenelse_equals_2 data()[124] 3.823s passed
disjointWithSingleton1 data()[125] 3.785s passed
disjointWithSingleton2 data()[126] 3.783s passed
disjointArrayRanges data()[127] 3.935s passed
disjointArrayRangeAllFields1 data()[128] 3.738s passed
disjointArrayRangeAllFields2 data()[129] 3.819s passed
div_unique1 data()[12] 4.000s passed
seqSelfDefinition data()[130] 3.786s passed
seqOutsideValue data()[131] 3.816s passed
castedGetAny data()[132] 4.182s passed
seqGetAlphaCast data()[133] 4.204s passed
getOfSeqSingleton data()[134] 3.881s passed
getOfSeqSingletonConcrete data()[135] 3.710s passed
getOfSeqConcat data()[136] 3.951s passed
getOfSeqSub data()[137] 3.835s passed
getOfSeqReverse data()[138] 3.771s passed
lenOfSeqEmpty data()[139] 3.723s passed
div_unique2 data()[13] 3.844s passed
lenOfSeqSingleton data()[140] 3.926s passed
lenOfSeqConcat data()[141] 3.831s passed
lenOfSeqSub data()[142] 3.800s passed
lenOfSeqReverse data()[143] 3.912s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.750s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.753s passed
getOfSeqSingletonEQ data()[146] 3.789s passed
getOfSeqConcatEQ data()[147] 3.933s passed
getOfSeqSubEQ data()[148] 3.872s passed
getOfSeqReverseEQ data()[149] 4.054s passed
div_exists data()[14] 4.023s passed
lenOfSeqEmptyEQ data()[150] 3.904s passed
lenOfSeqSingletonEQ data()[151] 3.861s passed
lenOfSeqConcatEQ data()[152] 3.809s passed
lenOfSeqSubEQ data()[153] 3.799s passed
lenOfSeqReverseEQ data()[154] 3.719s passed
getOfSeqDefEQ data()[155] 3.721s passed
lenOfSeqDefEQ data()[156] 3.902s passed
seqConcatWithSeqEmpty1 data()[157] 3.746s passed
seqConcatWithSeqEmpty2 data()[158] 3.810s passed
seqReverseOfSeqEmpty data()[159] 3.788s passed
div_one data()[15] 4.047s passed
subSeqComplete data()[160] 4.016s passed
subSeqTailR data()[161] 3.812s passed
subSeqTailL data()[162] 3.773s passed
subSeqTailEQR data()[163] 3.996s passed
subSeqTailEQL data()[164] 3.864s passed
seqDef_split data()[165] 3.819s passed
seqDef_induction_upper data()[166] 3.941s passed
seqDef_induction_upper_concrete data()[167] 3.875s passed
seqDef_induction_lower data()[168] 4.041s passed
seqDef_induction_lower_concrete data()[169] 4.272s passed
jdiv_one data()[16] 3.869s passed
seqDef_split_in_three data()[170] 4.216s passed
seqDef_empty data()[171] 3.969s passed
seqDef_one_summand data()[172] 4.105s passed
seqDef_lower_equals_upper data()[173] 3.793s passed
seqDefOfSeq data()[174] 3.801s passed
seqSelfDefinitionEQ2 data()[175] 3.756s passed
indexOfSeqSingleton data()[176] 3.811s passed
indexOfSeqConcatFirst data()[177] 3.800s passed
indexOfSeqConcatSecond data()[178] 3.797s passed
indexOfSeqSub data()[179] 3.783s passed
div_zero data()[17] 3.868s passed
lenOfArray2seq data()[180] 3.987s passed
getAnyOfArray2seq data()[181] 3.787s passed
getOfArray2seq data()[182] 3.796s passed
getAnyOfNPermInv data()[183] 4.034s passed
seqNPermRange data()[184] 3.896s passed
seqPermTrans data()[185] 3.913s passed
seqPermRefl data()[186] 3.813s passed
seqPermSplit data()[187] 3.757s passed
seqNPermRight data()[188] 3.983s passed
seqPermFromSwap data()[189] 3.879s passed
divResZero1 data()[18] 4.095s passed
seqPermTransAlt0 data()[190] 3.833s passed
seqPermTransAlt1 data()[191] 3.765s passed
seqPermTransAlt2 data()[192] 3.735s passed
seqPermTransAlt3 data()[193] 3.738s passed
seqPermForall data()[194] 3.980s passed
seqPermExists data()[195] 3.866s passed
schiffl_lemma_2 data()[196] 26.557s passed
schiffl_thm_1 data()[197] 4.717s passed
eqSameSeq data()[198] 4.250s passed
divResZero2 data()[19] 3.968s passed
eqTermCut data()[1] 4.499s passed
divResOne1 data()[20] 3.905s passed
divResOne2 data()[21] 3.847s passed
div_cancel1 data()[22] 4.181s passed
div_cancel2 data()[23] 3.818s passed
divAddMultDenom data()[24] 3.975s passed
divMinus data()[25] 3.984s passed
divMinusDenom data()[26] 3.899s passed
divLeastDPos data()[27] 4.123s passed
divLeastDNeg data()[28] 3.923s passed
divGreatestDPos data()[29] 3.922s passed
equivAllRight data()[2] 4.379s passed
divGreatestDNeg data()[30] 3.909s passed
divIncreasingPos data()[31] 4.054s passed
divIncreasingNeg data()[32] 3.899s passed
jdiv_zero data()[33] 3.808s passed
jdivPulloutMinusNum data()[34] 3.925s passed
jdivPulloutMinusDenom data()[35] 3.838s passed
jdiv_uniquePosPos data()[36] 3.806s passed
jdiv_uniquePosNeg data()[37] 4.009s passed
jdiv_uniqueNegPos data()[38] 3.921s passed
jdiv_uniqueNegNeg data()[39] 3.847s passed
irrflConcrete1 data()[3] 4.268s passed
jdivMultDenom1 data()[40] 3.821s passed
jdivMultDenom2 data()[41] 3.760s passed
mod_geZero data()[42] 3.799s passed
mod_lessDenom data()[43] 3.788s passed
jmod_NumPos data()[44] 3.904s passed
jmod_NumNeg data()[45] 3.732s passed
jmod_geZero data()[46] 3.923s passed
jmodNumZero data()[47] 3.921s passed
jmod_pulloutminusNum data()[48] 3.727s passed
jmod_pulloutminusDenom data()[49] 3.718s passed
irrflConcrete2 data()[4] 4.105s passed
jmodUnique1 data()[50] 3.898s passed
jmodUnique2 data()[51] 3.818s passed
intDivRem data()[52] 3.859s passed
jmodjmod data()[53] 3.850s passed
jmodDivisible data()[54] 3.774s passed
jmodDivisibleRep data()[55] 3.912s passed
jdivAddMultDenom data()[56] 4.126s passed
jmodAltZero data()[57] 3.952s passed
jmodAddMultDenomZero data()[58] 3.758s passed
polyDiv_zero data()[59] 3.795s passed
cancel_gtPos data()[5] 4.179s passed
polyMod_ltdivDenom data()[60] 3.735s passed
bsum_empty data()[61] 3.708s passed
bsum_induction_upper data()[62] 3.729s passed
bsum_induction_lower data()[63] 3.808s passed
bsum_num_of_bounds data()[64] 3.776s passed
bsum_num_of_bounds2 data()[65] 3.879s passed
bsum_induction_upper2 data()[66] 3.729s passed
bsum_induction_upper_concrete data()[67] 3.793s passed
bsum_induction_upper_concrete_2 data()[68] 3.927s passed
bsum_induction_upper2_concrete data()[69] 3.768s passed
cancel_gtNeg data()[6] 4.286s passed
bsum_induction_lower_concrete data()[70] 3.727s passed
bsum_induction_lower2 data()[71] 3.727s passed
bsum_induction_lower2_concrete data()[72] 3.770s passed
bsum_positive data()[73] 3.789s passed
bsum_upper_bound data()[74] 3.873s passed
bsum_lower_bound data()[75] 3.777s passed
bsum_positive_lower_bound_element data()[76] 3.892s passed
bsum_sub_same_index data()[77] 3.839s passed
bsum_less_same_index data()[78] 4.052s passed
bsum_equal_except_one_index data()[79] 3.759s passed
moduloIntIsInInt data()[7] 4.297s passed
bsum_num_of_is_max data()[80] 3.880s passed
bsum_num_of_is_max2 data()[81] 3.779s passed
bsum_num_of_is_max3 data()[82] 3.925s passed
bsum_num_of_is_max4 data()[83] 3.779s passed
bsum_num_of_lt_max data()[84] 3.766s passed
bsum_num_of_lt_max2 data()[85] 3.995s passed
bsum_num_of_lt_max3 data()[86] 3.808s passed
bsum_num_of_lt_max4 data()[87] 3.780s passed
bsum_num_of_gt0 data()[88] 3.794s passed
bsum_num_of_gt0_alt data()[89] 3.911s passed
moduloLongIsInLong data()[8] 4.387s passed
bsum_add_concrete data()[90] 3.899s passed
bprod_all_positive data()[91] 3.930s passed
bprod_split data()[92] 3.766s passed
powConcrete0 data()[93] 3.773s passed
powConcrete1 data()[94] 3.719s passed
powSplitFactor data()[95] 3.761s passed
powAdd data()[96] 3.857s passed
powMono data()[97] 3.791s passed
powMonoConcrete data()[98] 3.789s passed
powMonoConcreteRight data()[99] 3.729s passed
moduloShortIsInShort data()[9] 4.192s passed

Standard output

545        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
570        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.4ms 
819        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
835        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)

2246       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2248       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2252       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2253       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3875       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10412      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.59s 
10482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10521      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.9ns 
10534      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10535      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.02ns 
10540      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13861      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
13864      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15025      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.79ms 
15040      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15040      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.22ns 
15042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18136      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
18136      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
19381      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19415      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.08ms 
19424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19424      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.31ns 
19431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
22658      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
23681      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
23689      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
23699      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23700      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 556.24ns 
23704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26707      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
26708      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
27777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
27792      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms 
27800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
27801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.6ms 
27805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30924      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
30925      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
31929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
31976      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.06ms 
31980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
31981      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 779.15ns 
31982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35144      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
35145      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
36223      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
36263      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.65ms 
36265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
36265      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.01ns 
36266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39452      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
39452      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
40554      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
40560      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
40563      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
40564      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 520.13ns 
40566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
43850      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
44943      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
44947      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.05ns 
44951      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
44952      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.23ns 
44953      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48109      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
48109      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
49137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
49140      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.75ns 
49144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
49144      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 588.64ns 
49146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52441      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
52443      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
53510      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
53515      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 766.65ns 
53522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
53522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 487.63ns 
53524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56559      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
56560      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
57508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
57511      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.94ns 
57515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
57516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420.23ns 
57517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60379      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
60380      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
61411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
61513      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.83ms 
61515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
61515      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.11ns 
61516      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64406      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
64406      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
65321      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
65356      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.13ms 
65359      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
65359      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.01ns 
65360      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68231      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
68231      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
69146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
69378      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 224.25ms 
69383      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
69383      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.82ns 
69384      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72416      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
72417      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
73419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
73426      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
73431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
73432      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 583.44ns 
73434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76379      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
76380      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
77294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
77297      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
77301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
77302      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.62ns 
77303      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80196      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
80196      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
81109      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
81166      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.68ms 
81170      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
81170      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.41ns 
81171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84240      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
84240      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
85243      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
85263      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.18ms 
85266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
85266      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.03ns 
85267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
88237      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
89214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
89230      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.11ms 
89232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
89233      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.61ns 
89234      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92122      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
92122      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
93117      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
93135      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.24ms 
93138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
93139      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.83ns 
93140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95965      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
95967      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
96960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
96983      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.85ms 
96987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
96988      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 661.94ns 
96990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
100091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
101117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
101164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.17ms 
101168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
101168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.13ns 
101170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
104044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
104980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
104983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
104985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
104985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.71ns 
104986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
107897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
108910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
108957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.83ms 
108960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
108961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 577.54ns 
108962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
111937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
112877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
112941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.11ms 
112945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
112945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.33ns 
112947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
115771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
116736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
116841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.38ms 
116846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
116848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.46ms 
116850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
119956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
120954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
120966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ms 
120968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
120968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.42ns 
120972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
123857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
124866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
124889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.6ms 
124895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
124897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.95ms 
124900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
127838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
128800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
128813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.98ms 
128815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
128815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.91ns 
128816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
131779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
132712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
132722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.07ms 
132724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
132724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.52ns 
132725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
135744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
136763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
136775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ms 
136779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
136780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.52ns 
136781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
139763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
140667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
140676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 
140677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
140677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.11ns 
140678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
143556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
144480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
144484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
144487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
144487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.02ns 
144488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
147409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
148392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
148408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
148413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
148414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.93ns 
148415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
151275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
152181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
152249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.73ms 
152252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
152252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.32ns 
152254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
155099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
156033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
156056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.54ms 
156058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
156058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.21ns 
156059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
159059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
160023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
160064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.01ms 
160067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
160068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.63ns 
160069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
163037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
163966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
163986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.93ms 
163987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
163988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.31ns 
163988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
166801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
167808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
167834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.95ms 
167835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
167835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.41ns 
167836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
170663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
171609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
171654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.31ms 
171656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
171656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.81ns 
171657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
174451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
175411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
175414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
175415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
175415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.91ns 
175416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
178281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
179208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
179213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
179215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
179215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.21ns 
179216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
182007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
182987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
182998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.41ms 
183004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
183005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.63ns 
183006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
185972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
186896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
186906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ms 
186907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
186907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.61ns 
186908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
189683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
190616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
190637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.83ms 
190638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
190638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.11ns 
190639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
193542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
194551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
194560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.57ms 
194562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
194562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.11ns 
194563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
197466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
198477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
198481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
198484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
198484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.82ns 
198485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
201278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
202204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
202208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
202210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
202210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.21ns 
202210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
204995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
205922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
205926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
205928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
205928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.51ns 
205929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
208809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
209746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
209824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.21ms 
209826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
209826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.11ns 
209827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
212647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
213546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
213642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.12ms 
213644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
213644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.61ns 
213645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
216573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
217491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
217500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
217503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
217503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.81ns 
217505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
220409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
221311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
221351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.33ms 
221353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
221354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.32ns 
221355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
224193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
225091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
225125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.46ms 
225127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
225127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.91ns 
225128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
227990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
229033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
229037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
229040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
229040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.33ns 
229042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
232051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
232997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
233162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 152.8ms 
233165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
233165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.52ns 
233166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
236064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
237100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
237115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
237117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
237117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
237118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
239935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
240865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
240874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.49ms 
240875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
240875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.01ns 
240876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
243725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
244649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
244668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.82ms 
244669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
244670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.61ns 
244670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
247467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
248389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
248403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.58ms 
248405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
248405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.81ns 
248406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
251185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
252107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
252111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
252113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
252113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.71ns 
252114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
254909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
255835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
255840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
255842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
255842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.81ns 
255843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
258674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
259619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
259648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.97ms 
259650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
259650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.61ns 
259651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
262473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
263405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
263424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.25ms 
263426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
263426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
263427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
266306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
267285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
267303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.69ms 
267305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
267305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.01ns 
267305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
270105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
271028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
271032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
271034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
271034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
271035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
273807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
274819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
274825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
274826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
274826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.11ns 
274827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
277808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
278746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
278752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
278753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
278753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.21ns 
278754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
281619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
282517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
282520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
282522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
282522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.91ns 
282523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
285346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
286244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
286247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 790.75ns 
286248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
286249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.91ns 
286249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
289070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
289970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
289974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
289976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
289976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.61ns 
289977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
292846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
293741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
293744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
293745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
293745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
293746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
296540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
297448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
297532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.47ms 
297535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
297536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.42ns 
297537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
300440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
301350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
301406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.97ms 
301407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
301408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.21ns 
301409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
304208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
305136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
305183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.28ms 
305184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
305184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.91ns 
305185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
308009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
308997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
309075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.82ms 
309077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
309077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.71ns 
309078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
311942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
312877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
312915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.44ms 
312916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
312916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.81ns 
312917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
315982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
316908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
316966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.44ms 
316968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
316968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.31ns 
316969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
319765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
320693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
320725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.19ms 
320726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
320727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.51ns 
320727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
323656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
324582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
324605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms 
324607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
324607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.81ns 
324608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
327387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
328352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
328384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.05ms 
328385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
328386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.31ns 
328386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
331318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
332285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
332309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.65ms 
332311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
332311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.01ns 
332312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
335119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
336055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
336088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.85ms 
336091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
336091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.82ns 
336092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
338880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
339825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
339854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.44ms 
339855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
339855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.11ns 
339865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
342829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
343817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
343849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.93ms 
343851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
343851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.71ns 
343852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
346684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
347628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
347657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.71ms 
347659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
347659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.51ns 
347660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
350514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
351413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
351437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.14ms 
351439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
351439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.51ns 
351440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
354285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
355204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
355231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.07ms 
355233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
355233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
355234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
358206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
359114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
359142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.12ms 
359144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
359144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.31ns 
359145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
362096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
363030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
363042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms 
363043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
363043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.81ns 
363044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
366016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
366942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
366971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.09ms 
366972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
366973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.01ns 
366977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
369800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
370733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
370738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
370739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
370739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
370740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
373566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
374508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
374510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.14ns 
374512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
374512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
374513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
377297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
378227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
378229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 857.55ns 
378231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
378231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.11ns 
378232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
381048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
381977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
381990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
381993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
381993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.21ns 
381994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
384842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
385840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
385848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
385850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
385858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.18ms 
385860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
388696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
389625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
389639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.51ms 
389640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
389641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.41ns 
389641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
392488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
393424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
393428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
393429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
393429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
393430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
396224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
397155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
397157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 603.14ns 
397158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
397159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.91ns 
397159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
400042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
400968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
400975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
400976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
400976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.11ns 
400977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
403769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
404695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
404698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720.35ns 
404699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
404699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
404700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
407516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
408443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
408446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665.24ns 
408447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
408447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
408448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
411367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
412296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
412298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.64ns 
412300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
412300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
412300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
415184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
416124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
416128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
416130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
416130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.91ns 
416130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
418922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
419886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
419896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.16ms 
419898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
419898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
419899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
422703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
423630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
423634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms 
423636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
423636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.31ns 
423638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
426451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
427352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
427360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
427362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
427362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.91ns 
427363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
430179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
431131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
431138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.07ms 
431143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
431144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 634.44ns 
431145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
434083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
435076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
435095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.89ms 
435096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
435096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
435097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
438025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
438989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
438994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
438995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
438995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
438996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
441931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
442884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
442888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
442889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
442889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.51ns 
442890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
445704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
446603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
446607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
446609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
446609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
446610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
449477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
450405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
450425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.24ms 
450427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
450427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
450427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
453262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
454204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
454213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.44ns 
454216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
454216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.72ns 
454217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
457058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
457981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
458028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.57ms 
458029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
458030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.11ns 
458030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
460813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
461744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
461748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
461749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
461749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
461750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
464581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
465512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
465538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.31ms 
465539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
465539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.41ns 
465540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
468332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
469341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
469369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.59ms 
469371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
469371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.11ns 
469372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
472375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
473303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
473331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.07ms 
473333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
473333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.41ns 
473334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
476151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
477112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
477116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.25ns 
477118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
477118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.62ns 
477119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
479941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
480915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
480922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.07ms 
480924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
480924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
480925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
483782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
484715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
484718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
484720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
484720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
484721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
487494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
488424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
488427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 944.56ns 
488429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
488429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
488429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
491213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
492247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
492250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
492252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
492252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
492253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
495093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
496031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
496035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
496037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
496037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.81ns 
496037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
498904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
499814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
499818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
499820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
499820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.11ns 
499821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
502837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
503741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
503753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.76ms 
503755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
503755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.11ns 
503755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
506561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
507477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
507491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.72ms 
507493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
507493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.61ns 
507494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
510367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
511299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
511311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.07ms 
511312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
511312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
511313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
514117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
515071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
515096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.23ms 
515099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
515099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.81ns 
515100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
517927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
518906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
518912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
518914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
518914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.71ns 
518915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
522022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
523087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
523095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms 
523096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
523096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.31ns 
523097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
526259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
527295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
527298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
527300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
527300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.61ns 
527301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
530240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
531175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
531179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
531181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
531181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
531181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
533978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
534886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
534889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
534890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
534890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
534891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
537796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
538826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
538840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.78ms 
538842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
538842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
538843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
541690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
542671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
542676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
542677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
542677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.81ns 
542678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
545501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
546439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
546447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
546448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
546448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.11ns 
546449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
549228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
550167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
550169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 901.56ns 
550171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
550171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
550172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
553138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
554093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
554095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 730.15ns 
554097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
554097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.11ns 
554098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
557003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
557922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
557926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
557928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
557928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.31ns 
557929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
560782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
561723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
561726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
561728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
561728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
561728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
564664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
565634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
565638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
565639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
565639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
565640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
568412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
569385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
569389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
569390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
569390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
569391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
572222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
573133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
573141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
573142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
573143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
573143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
575973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
576927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
576931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
576932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
576932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
576933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
579872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
580850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
580863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ms 
580864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
580865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.31ns 
580865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
583748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
584733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
584736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 797.65ns 
584737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
584737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
584738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
587810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
588780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
588790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.16ms 
588791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
588791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
588792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
591725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
592690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
592693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
592694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
592694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
592695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
595607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
596552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
596555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 869.56ns 
596556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
596556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
596557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
599445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
600357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
600363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
600364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
600364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
600365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
603222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
604159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
604162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
604164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
604164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
604165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
606941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
607878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
607881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
607883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
607883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
607884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
610687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
611599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
611603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
611604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
611604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
611605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
614534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
615498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
615504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
615505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
615506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.41ns 
615506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
618295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
619233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
619250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.51ms 
619251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
619252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.31ns 
619252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
622128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
623042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
623060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms 
623062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
623062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.21ns 
623063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
625884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
626832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
626848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.11ms 
626850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
626850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.81ns 
626851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
629911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
630852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
630865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.23ms 
630866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
630866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
630867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
633710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
634646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
634676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.2ms 
634677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
634678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
634678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
637482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
638420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
638449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.93ms 
638451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
638451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.31ns 
638452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
641444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
642418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
642445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.12ms 
642447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
642447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
642448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
645246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
646285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
646309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.88ms 
646311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
646311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.01ns 
646312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
649183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
650093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
650129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.12ms 
650130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
650130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.91ns 
650131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
653072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
654014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
654069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.49ms 
654070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
654071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
654072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
656983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
657898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
657944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.52ms 
657946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
657946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.51ns 
657947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
660908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
661932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
661985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.03ms 
661986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
661986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.91ns 
661987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
665189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
666202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
666257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.59ms 
666258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
666259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.21ns 
666260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
669321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
670318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
670473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 146.71ms 
670475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
670475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.21ns 
670476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
673435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
674433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
674442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.86ms 
674443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
674443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
674444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
677444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
678538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
678547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms 
678548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
678549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.41ns 
678549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
681387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
682335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
682341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
682342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
682342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.31ns 
682343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
685183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
686120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
686141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.4ms 
686142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
686142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.31ns 
686143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
688934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
689884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
689897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.61ms 
689898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
689899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.31ns 
689899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
692768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
693704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
693708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
693709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
693710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
693710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
696552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
697486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
697508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.89ms 
697510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
697511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.62ns 
697512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
700373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
701286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
701305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms 
701306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
701306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.81ns 
701307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
704131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
705066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
705089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.35ms 
705090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
705090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.61ns 
705091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
708066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
709072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
709076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
709077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
709077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.61ns 
709078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
711878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
712858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
712862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
712864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
712864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
712865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
715687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
716651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
716658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.58ms 
716660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
716660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.71ns 
716661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
719697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
720685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
720692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
720694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
720694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
720695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
723516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
724500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
724588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.44ms 
724590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
724590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.41ns 
724591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
727533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
728470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
728501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.49ms 
728502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
728503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
728503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
731312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
732287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
732314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.55ms 
732315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
732316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.61ns 
732316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
735134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
736069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
736071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 334.52ns 
736073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
736073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
736074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
738882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
739819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
740054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.58ms 
740056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
740057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.62ns 
740058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
742899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
743873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
743934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.31ms 
743935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
743935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.61ns 
743936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
746760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
747764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
747766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 407.33ns 
747768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
747768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
747768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
750618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
751530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
751532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 414.53ns 
751533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
751533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
751534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
754326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
755264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
755267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 457.23ns 
755268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
755268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.61ns 
755269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
758066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
759002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
759004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 647.95ns 
759005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
759005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.91ns 
759006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
761873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
762859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
762984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 122.86ms 
762986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
762987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.32ns 
762989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
765878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
766791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
766850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.75ms 
766851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
766851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.41ns 
766853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
769910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
770931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
770933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
770968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
771019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
771039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
771044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
771051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
771055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
771056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
771058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
771062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
771064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
771067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
771068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
771330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
771332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
771334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
771337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
771338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
771493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
771495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
771496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
771498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
771500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
771501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
771714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
771716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
771718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
771719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
771720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
771725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
771922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
771923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
771925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
771926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
771927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
771928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
771937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
771938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
771939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
771941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
771944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
771945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
771955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
771956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
771957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
771958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
771959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
771960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
772137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
772139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
772140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
772261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
772263     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)'' 
772265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
772267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
772268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
772270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
772270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
772273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
772276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
772278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
772280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
772280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
772281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
772388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
772391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
772393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
772394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
772395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
772396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
772398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
772525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
772527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
772528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
772529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
772530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
772531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
772532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
772534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
772627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
772629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
772751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
772755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
772763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
772764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
772765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
772768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
772771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
772772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
772772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
772780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
772790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
772797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
772907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
772909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
772911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
772913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
772914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
772914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
772915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
772916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
772976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
772983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
773087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
773090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
773092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
773094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
773095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
773096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
773249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
773253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
773257     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)'' 
773259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
773260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
773261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
773262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
773263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
773273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
773279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
773281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
773282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
773388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
773390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
773391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
773392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
773393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
773395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
773506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
773508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
773509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
773511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
773512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
773513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
773514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
773515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
773618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
773620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
773707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
773708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
773709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
773714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
773718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
773724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
773871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
773874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
773875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
773876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
773889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
773986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
778029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
778030     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)'' 
778036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
778038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
778039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
778039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
778041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
778053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
778055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
778057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
778058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
778058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
778176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
778180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
778182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
778182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
778184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
778185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
778186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
778305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
778307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
778308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
778309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
778310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
778311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
778311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
778312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
778400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
778402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
778488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
778493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
778497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
778499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
778500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
778501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
778512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
778608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
778609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
778610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
778611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
778695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
778706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
778707     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)'' 
778709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
778710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
778711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
778712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
778712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
778725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
778727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
778728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
778729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
778729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
778832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
778834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
778835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
778836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
778837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
778943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
778948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
778950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
778951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
778951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
778952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
778953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
779069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
779071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
779073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
779075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
779076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
779076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
779077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
779078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
779079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
779080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
779082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
779082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
779083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
779084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
779085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
779186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
779188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
779195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
779286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
779387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
779388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
779390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
779391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
779392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
779393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
779393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
779394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
779395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
779498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
779505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
779610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
779612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
779612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
779614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
779614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
779615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
779615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
779616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
779622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
779623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
779717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
779723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
779729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
779903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
779904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
779905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
779906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
779907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
779907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
779907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
779908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
779971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
779972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
779973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
779974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
779975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
779981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
779987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
780123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
780224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
780226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
780226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
780227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
780420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
780521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
780522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
784138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
784143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
784145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
784146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
784147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
784342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
784343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
784345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
784346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
784347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
784470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
787929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
791874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
791880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
791881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
791882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
791883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
792026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
792028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
792029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
792031     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)' ...' 
792032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
793408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
793409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.81ns 
793409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
796336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
796336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
797313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
797314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
797315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
797324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
797337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
797340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
797342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
797343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
797348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
797350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
797353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
797356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
797357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
797368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
797370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
797370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
797423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
797424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
797425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
797425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
797426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
797501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
797502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
797503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
797504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
797505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
797509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
797510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
797510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
797511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
797513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
797513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
797604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
797605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
797606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
797608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
797609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
797609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
797709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
797710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
797711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
797712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
797712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
797714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
797714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
797715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
797716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
797717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
797717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
797718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
797719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
797719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
797720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
797721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
797721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
797722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
797724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
797726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
797771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
797773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
797844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
797846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
797847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
797849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
797850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
797851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
797910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
797913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
797914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
797916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
797918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
797919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
797919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
797976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
797979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
797983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
798054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
798127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
798127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.92ns 
798128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
801277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
802333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
802374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.61ms