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

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

tests
0

failures
0

ignored
13m46.59s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.984s passed
powPositiveConcrete data()[101] 3.971s passed
powGeq1Concrete data()[102] 3.981s passed
pow2InIntLower data()[103] 3.937s passed
pow2InIntUpper data()[104] 3.963s passed
logSelfConcrete data()[105] 3.971s passed
log1Concrete data()[106] 3.946s passed
logProduct data()[107] 3.999s passed
logTimesBaseConcrete data()[108] 3.969s passed
logProdIdentity data()[109] 3.947s passed
moduloByteIsInByte data()[10] 4.148s passed
logProdIdentityConcrete data()[110] 3.944s passed
logPowIdentity data()[111] 3.923s passed
logPowIdentityConcrete data()[112] 3.965s passed
logPositive data()[113] 3.974s passed
logPositiveConcrete data()[114] 3.995s passed
logMono data()[115] 4.001s passed
logMonoConcrete data()[116] 3.968s passed
powLogLess data()[117] 4.023s passed
powLogMore2 data()[118] 3.995s passed
logLessThanPow data()[119] 3.986s passed
moduloCharIsInChar data()[11] 4.045s passed
logLessThanPowConcrete data()[120] 4.021s passed
logSqueeze data()[121] 3.921s passed
ifthenelse_equals data()[122] 3.965s passed
ifthenelse_equals_1 data()[123] 3.932s passed
ifthenelse_equals_2 data()[124] 4.025s passed
disjointWithSingleton1 data()[125] 3.978s passed
disjointWithSingleton2 data()[126] 3.982s passed
disjointArrayRanges data()[127] 3.981s passed
disjointArrayRangeAllFields1 data()[128] 4.064s passed
disjointArrayRangeAllFields2 data()[129] 3.952s passed
div_unique1 data()[12] 4.150s passed
seqSelfDefinition data()[130] 4.038s passed
seqOutsideValue data()[131] 4.010s passed
castedGetAny data()[132] 4.064s passed
seqGetAlphaCast data()[133] 4.048s passed
getOfSeqSingleton data()[134] 3.997s passed
getOfSeqSingletonConcrete data()[135] 4.011s passed
getOfSeqConcat data()[136] 4.042s passed
getOfSeqSub data()[137] 3.975s passed
getOfSeqReverse data()[138] 4.003s passed
lenOfSeqEmpty data()[139] 3.949s passed
div_unique2 data()[13] 4.197s passed
lenOfSeqSingleton data()[140] 3.983s passed
lenOfSeqConcat data()[141] 3.998s passed
lenOfSeqSub data()[142] 4.006s passed
lenOfSeqReverse data()[143] 3.983s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.031s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.005s passed
getOfSeqSingletonEQ data()[146] 4.017s passed
getOfSeqConcatEQ data()[147] 4.057s passed
getOfSeqSubEQ data()[148] 4.035s passed
getOfSeqReverseEQ data()[149] 3.990s passed
div_exists data()[14] 4.337s passed
lenOfSeqEmptyEQ data()[150] 4.014s passed
lenOfSeqSingletonEQ data()[151] 3.978s passed
lenOfSeqConcatEQ data()[152] 3.995s passed
lenOfSeqSubEQ data()[153] 4.061s passed
lenOfSeqReverseEQ data()[154] 4.004s passed
getOfSeqDefEQ data()[155] 4.016s passed
lenOfSeqDefEQ data()[156] 4.016s passed
seqConcatWithSeqEmpty1 data()[157] 4.026s passed
seqConcatWithSeqEmpty2 data()[158] 4.051s passed
seqReverseOfSeqEmpty data()[159] 4.029s passed
div_one data()[15] 4.029s passed
subSeqComplete data()[160] 4.004s passed
subSeqTailR data()[161] 4.068s passed
subSeqTailL data()[162] 4.095s passed
subSeqTailEQR data()[163] 4.092s passed
subSeqTailEQL data()[164] 4.034s passed
seqDef_split data()[165] 4.019s passed
seqDef_induction_upper data()[166] 4.054s passed
seqDef_induction_upper_concrete data()[167] 4.026s passed
seqDef_induction_lower data()[168] 4.049s passed
seqDef_induction_lower_concrete data()[169] 4.023s passed
jdiv_one data()[16] 4.058s passed
seqDef_split_in_three data()[170] 4.157s passed
seqDef_empty data()[171] 4.006s passed
seqDef_one_summand data()[172] 3.942s passed
seqDef_lower_equals_upper data()[173] 3.996s passed
seqDefOfSeq data()[174] 3.982s passed
seqSelfDefinitionEQ2 data()[175] 3.968s passed
indexOfSeqSingleton data()[176] 4.013s passed
indexOfSeqConcatFirst data()[177] 4.020s passed
indexOfSeqConcatSecond data()[178] 3.989s passed
indexOfSeqSub data()[179] 3.986s passed
div_zero data()[17] 4.086s passed
lenOfArray2seq data()[180] 3.993s passed
getAnyOfArray2seq data()[181] 4.000s passed
getOfArray2seq data()[182] 4.013s passed
getAnyOfNPermInv data()[183] 3.990s passed
seqNPermRange data()[184] 4.084s passed
seqPermTrans data()[185] 4.097s passed
seqPermRefl data()[186] 3.990s passed
seqPermSplit data()[187] 3.985s passed
seqNPermRight data()[188] 4.345s passed
seqPermFromSwap data()[189] 4.136s passed
divResZero1 data()[18] 4.078s passed
seqPermTransAlt0 data()[190] 4.013s passed
seqPermTransAlt1 data()[191] 3.949s passed
seqPermTransAlt2 data()[192] 4.020s passed
seqPermTransAlt3 data()[193] 3.982s passed
seqPermForall data()[194] 4.128s passed
seqPermExists data()[195] 4.084s passed
schiffl_lemma_2 data()[196] 29.567s passed
schiffl_thm_1 data()[197] 5.110s passed
eqSameSeq data()[198] 4.299s passed
divResZero2 data()[19] 4.053s passed
eqTermCut data()[1] 4.984s passed
divResOne1 data()[20] 4.054s passed
divResOne2 data()[21] 4.103s passed
div_cancel1 data()[22] 4.031s passed
div_cancel2 data()[23] 4.034s passed
divAddMultDenom data()[24] 4.092s passed
divMinus data()[25] 4.119s passed
divMinusDenom data()[26] 4.132s passed
divLeastDPos data()[27] 4.079s passed
divLeastDNeg data()[28] 4.053s passed
divGreatestDPos data()[29] 4.021s passed
equivAllRight data()[2] 4.625s passed
divGreatestDNeg data()[30] 4.070s passed
divIncreasingPos data()[31] 4.015s passed
divIncreasingNeg data()[32] 4.092s passed
jdiv_zero data()[33] 4.017s passed
jdivPulloutMinusNum data()[34] 4.021s passed
jdivPulloutMinusDenom data()[35] 4.088s passed
jdiv_uniquePosPos data()[36] 4.054s passed
jdiv_uniquePosNeg data()[37] 4.176s passed
jdiv_uniqueNegPos data()[38] 3.989s passed
jdiv_uniqueNegNeg data()[39] 4.012s passed
irrflConcrete1 data()[3] 4.393s passed
jdivMultDenom1 data()[40] 4.060s passed
jdivMultDenom2 data()[41] 4.000s passed
mod_geZero data()[42] 4.069s passed
mod_lessDenom data()[43] 4.018s passed
jmod_NumPos data()[44] 3.999s passed
jmod_NumNeg data()[45] 4.054s passed
jmod_geZero data()[46] 3.990s passed
jmodNumZero data()[47] 4.008s passed
jmod_pulloutminusNum data()[48] 3.965s passed
jmod_pulloutminusDenom data()[49] 3.970s passed
irrflConcrete2 data()[4] 4.313s passed
jmodUnique1 data()[50] 4.142s passed
jmodUnique2 data()[51] 4.137s passed
intDivRem data()[52] 3.999s passed
jmodjmod data()[53] 4.068s passed
jmodDivisible data()[54] 4.047s passed
jmodDivisibleRep data()[55] 3.975s passed
jdivAddMultDenom data()[56] 4.273s passed
jmodAltZero data()[57] 4.029s passed
jmodAddMultDenomZero data()[58] 3.968s passed
polyDiv_zero data()[59] 4.070s passed
cancel_gtPos data()[5] 4.281s passed
polyMod_ltdivDenom data()[60] 3.962s passed
bsum_empty data()[61] 3.968s passed
bsum_induction_upper data()[62] 4.029s passed
bsum_induction_lower data()[63] 4.005s passed
bsum_num_of_bounds data()[64] 3.991s passed
bsum_num_of_bounds2 data()[65] 4.083s passed
bsum_induction_upper2 data()[66] 3.961s passed
bsum_induction_upper_concrete data()[67] 3.991s passed
bsum_induction_upper_concrete_2 data()[68] 3.979s passed
bsum_induction_upper2_concrete data()[69] 3.931s passed
cancel_gtNeg data()[6] 4.251s passed
bsum_induction_lower_concrete data()[70] 3.964s passed
bsum_induction_lower2 data()[71] 3.995s passed
bsum_induction_lower2_concrete data()[72] 4.054s passed
bsum_positive data()[73] 4.032s passed
bsum_upper_bound data()[74] 4.031s passed
bsum_lower_bound data()[75] 4.103s passed
bsum_positive_lower_bound_element data()[76] 4.013s passed
bsum_sub_same_index data()[77] 4.027s passed
bsum_less_same_index data()[78] 4.028s passed
bsum_equal_except_one_index data()[79] 3.988s passed
moduloIntIsInInt data()[7] 4.196s passed
bsum_num_of_is_max data()[80] 4.031s passed
bsum_num_of_is_max2 data()[81] 4.001s passed
bsum_num_of_is_max3 data()[82] 4.017s passed
bsum_num_of_is_max4 data()[83] 3.976s passed
bsum_num_of_lt_max data()[84] 3.969s passed
bsum_num_of_lt_max2 data()[85] 3.982s passed
bsum_num_of_lt_max3 data()[86] 4.025s passed
bsum_num_of_lt_max4 data()[87] 4.039s passed
bsum_num_of_gt0 data()[88] 4.009s passed
bsum_num_of_gt0_alt data()[89] 4.070s passed
moduloLongIsInLong data()[8] 4.128s passed
bsum_add_concrete data()[90] 4.052s passed
bprod_all_positive data()[91] 3.977s passed
bprod_split data()[92] 3.994s passed
powConcrete0 data()[93] 3.930s passed
powConcrete1 data()[94] 3.949s passed
powSplitFactor data()[95] 3.979s passed
powAdd data()[96] 3.970s passed
powMono data()[97] 3.987s passed
powMonoConcrete data()[98] 4.034s passed
powMonoConcreteRight data()[99] 3.929s passed
moduloShortIsInShort data()[9] 4.083s passed

Standard output

573        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
599        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.69ms 
899        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
926        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)

2169       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2171       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2174       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2174       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3833       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10343      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.44s 
10446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10497      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.8ns 
10516      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10518      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.83ms 
10524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14198      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 
14201      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15484      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.5ms 
15503      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15503      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.62ns 
15506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
18978      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20126      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms 
20129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20130      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 429.13ns 
20131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23477      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
23479      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24519      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 
24525      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24526      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.42ns 
24527      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27726      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
27727      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
28816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
28834      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.58ms 
28838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
28838      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.71ns 
28839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
32022      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
33063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
33116      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.47ms 
33119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
33120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.02ns 
33123      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
36335      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
37337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
37368      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.68ms 
37371      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
37372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.82ns 
37373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40491      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
40493      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
41561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
41565      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 777.35ns 
41568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
41568      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.52ns 
41570      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44675      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
44675      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
45687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
45693      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.84ns 
45696      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
45696      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 520.03ns 
45698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48775      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
48775      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
49774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
49777      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.24ns 
49780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
49780      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 460.13ns 
49782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52877      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
52878      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
53922      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
53925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 767.54ns 
53929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
53929      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.11ns 
53931      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56984      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
56984      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
57969      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
57971      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.84ns 
57975      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
57975      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.02ns 
57977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61058      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
61059      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
62062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
62122      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.75ms 
62128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
62129      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 693.34ns 
62130      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65274      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
65275      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
66233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
66320      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.49ms 
66325      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
66325      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.72ns 
66328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69393      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
69393      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
70403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
70657      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 244.64ms 
70662      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
70663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 430.12ns 
70664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73694      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
73694      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
74682      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
74688      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
74692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
74692      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 675.84ns 
74694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77761      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
77763      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
78743      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
78747      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
78751      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
78751      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 641.24ns 
78753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81786      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
81786      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
82779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
82834      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.29ms 
82838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
82838      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.22ns 
82839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85921      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
85922      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
86889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
86914      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.39ms 
86916      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
86917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.92ns 
86918      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89962      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
89962      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
90945      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
90967      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.51ms 
90971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
90971      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.91ns 
90976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93971      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
93971      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
94986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
95019      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.74ms 
95026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
95027      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485.73ns 
95028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
98121      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
99063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
99125      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.57ms 
99128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
99129      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.12ns 
99130      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
102153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
103120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
103156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.08ms 
103159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
103159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.82ns 
103160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
106208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
107187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
107191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
107192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
107193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.51ns 
107194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
110218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
111222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
111283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.32ms 
111285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
111286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.32ns 
111287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
114333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
115316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
115402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.45ms 
115404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
115404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.71ns 
115406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
118463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
119425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
119534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.76ms 
119540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
119543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.94ms 
119545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
122635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
123605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
123615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.69ms 
123616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
123616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.51ns 
123617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
126653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
127648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
127667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.73ms 
127669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
127669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.41ns 
127670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
130689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
131670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
131688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.86ms 
131690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
131691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.52ns 
131692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
134782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
135746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
135757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.06ms 
135760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
135760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.51ns 
135761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
138793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
139761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
139773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.78ms 
139776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
139776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.42ns 
139778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
142875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
143850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
143865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.49ms 
143868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
143868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.32ns 
143869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
146888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
147877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
147882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
147884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
147885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.52ns 
147886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
150905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
151887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
151903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.34ms 
151905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
151905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.31ns 
151906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
154906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
155896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
155991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.04ms 
155994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
155994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.42ns 
155997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
159080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
160019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
160046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.8ms 
160048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
160049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 583.83ns 
160050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
163205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
164191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
164222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.39ms 
164225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
164225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.52ns 
164226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
167218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
168183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
168211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.5ms 
168213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
168213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.81ns 
168214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
171217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
172196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
172223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.39ms 
172225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
172225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.41ns 
172226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
175211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
176213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
176283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.77ms 
176284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
176284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.51ns 
176285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
179312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
180275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
180283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
180284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
180285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.31ns 
180286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
183342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
184346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
184352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
184354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
184354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.11ns 
184355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
187374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
188359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
188370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
188372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
188372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
188373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
191377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
192357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
192370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 
192371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
192371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
192372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
195397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
196393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
196423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.86ms 
196425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
196425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.41ns 
196426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
199447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
200402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
200414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
200416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
200416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
200417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
203409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
204417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
204421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
204424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
204424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.62ns 
204425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
207410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
208382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
208387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
208388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
208388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.11ns 
208389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
211402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
212350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
212356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
212357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
212357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
212358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
215385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
216372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
216497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 116.51ms 
216500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
216501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.61ns 
216502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
219489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
220485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
220635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 139.55ms 
220637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
220638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.61ns 
220639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
223650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
224628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
224634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
224636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
224637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.92ns 
224638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
227657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
228640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
228701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.7ms 
228704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
228705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.02ms 
228706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
231748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
232700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
232749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.59ms 
232751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
232752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.12ns 
232753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
235760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
236719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
236724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
236726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
236727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
236728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
239740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
240728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
240998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 258.1ms 
241000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
241000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.71ns 
241001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
244053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
245010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
245027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.84ms 
245029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
245031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.41ns 
245032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
248018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
248983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
248995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.88ms 
248997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
248997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
248998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
252047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
253035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
253065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.67ms 
253067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
253067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.71ns 
253068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
256049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
257007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
257025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.39ms 
257029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
257030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.81ns 
257031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
260041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
260992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
260996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
260998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
260998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
260999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
264035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
265019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
265026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
265027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
265027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
265028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
268018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
268990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
269030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.14ms 
269032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
269032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
269033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
272042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
272993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
273021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.67ms 
273023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
273023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
273024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
276110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
277076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
277102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.95ms 
277107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
277107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.51ns 
277108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
280099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
281058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
281065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
281067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
281067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
281068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
284073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
285048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
285056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.45ms 
285058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
285059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.31ns 
285059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
288058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
289027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
289036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.92ms 
289038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
289038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
289039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
292022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
292962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
292967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
292969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
292969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.01ns 
292970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
295966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
296928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
296931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
296933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
296933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
296934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
299941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
300920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
300926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
300928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
300928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
300929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
303957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
304976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
304981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
304982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
304982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
304983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
307955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
308943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
309012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.92ms 
309014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
309014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.31ns 
309015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
311996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
312969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
313042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.82ms 
313045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
313045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.21ns 
313046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
316106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
317093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
317146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.66ms 
317147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
317148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
317148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
320119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
321091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
321159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.74ms 
321161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
321161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.21ns 
321162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
324178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
325138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
325186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.93ms 
325188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
325188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
325189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
328163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
329125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
329213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.05ms 
329216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
329216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.51ns 
329217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
332222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
333152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
333202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.54ms 
333204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
333204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
333207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
336241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
337198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
337232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.72ms 
337235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
337235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.31ns 
337236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
340213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
341190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
341233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.86ms 
341236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
341237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.61ns 
341238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
344256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
345216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
345251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.85ms 
345253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
345253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.91ns 
345255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
348209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
349177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
349228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.49ms 
349229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
349229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.81ns 
349232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
352215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
353154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
353196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.33ms 
353198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
353198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.21ns 
353199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
356180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
357135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
357178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.25ms 
357180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
357180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
357181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
360160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
361160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
361203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.09ms 
361205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
361205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
361206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
364248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
365210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
365243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.8ms 
365244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
365244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
365245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
368214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
369216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
369252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.76ms 
369253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
369253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.81ns 
369254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
372330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
373285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
373321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.12ms 
373323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
373323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
373324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
376365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
377362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
377373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
377374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
377374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.91ns 
377375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
380352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
381326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
381350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.22ms 
381352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
381352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
381352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
384367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
385340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
385345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
385346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
385346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
385347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
388310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
389271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
389274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.34ns 
389276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
389276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.21ns 
389277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
392285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
393221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
393224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 889.34ns 
393225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
393225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
393226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
396228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
397192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
397202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
397204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
397204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
397205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
400200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
401163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
401172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
401174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
401175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 632.83ns 
401175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
404188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
405141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
405159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.06ms 
405161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
405162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.41ns 
405163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
408227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
409189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
409193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
409194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
409194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
409195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
412146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
413120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
413123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.83ns 
413124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
413124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
413125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
416131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
417099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
417107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.38ms 
417108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
417108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
417109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
420090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
421075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
421077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.93ns 
421079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
421079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
421080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
424096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
425055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
425058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 810.03ns 
425060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
425060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
425060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
428034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
428993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
428995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.94ns 
428997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
428997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105ns 
428998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
431980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
432950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
432958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
432960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
432960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
432960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
435963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
436917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
436929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.35ms 
436930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
436931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
436931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
439894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
440871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
440875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
440877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
440877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
440878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
443916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
444858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
444875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.84ms 
444876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
444876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
444877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
447870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
448839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
448844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
448845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
448845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
448846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
451809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
452769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
452790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.78ms 
452791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
452792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
452792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
455761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
456730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
456735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
456736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
456736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
456737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
459690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
460654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
460658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
460659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
460659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
460660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
463639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
464617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
464622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
464624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
464624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
464625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
467611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
468573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
468597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.36ms 
468599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
468599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.71ns 
468600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
471627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
472585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
472591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 661.83ns 
472594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
472594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
472598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
475555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
476531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
476593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.75ms 
476594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
476594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.91ns 
476595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
479557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
480557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
480561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
480563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
480563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
480564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
483586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
484554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
484584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.82ms 
484585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
484586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
484586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
487593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
488549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
488579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.45ms 
488581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
488581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
488582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
491566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
492530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
492565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.19ms 
492569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
492569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.61ns 
492570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
495602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
496584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
496587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 775.33ns 
496589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
496589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
496590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
499542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
500500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
500508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.58ms 
500511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
500511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.2ns 
500512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
503492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
504470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
504473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
504475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
504475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
504475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
507463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
508403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
508406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 999.34ns 
508407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
508407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
508408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
511447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
512427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
512430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
512433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
512433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
512433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
515432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
516406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
516410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
516411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
516411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
516412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
519414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
520388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
520391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
520393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
520393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
520394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
523378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
524358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
524372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.88ms 
524379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
524382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.52ms 
524383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
527442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
528393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
528440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.04ms 
528442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
528442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.11ns 
528443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
531382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
532374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
532390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.08ms 
532394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
532394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
532395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
535414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
536405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
536430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.67ms 
536432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
536432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
536433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
539452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
540435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
540441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
540442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
540442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
540443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
543487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
544496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
544504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.46ms 
544506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
544506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
544507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
547541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
548550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
548553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.14ns 
548554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
548554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
548555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
551554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
552545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
552549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
552550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
552551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
552551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
555570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
556558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
556561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
556562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
556562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
556563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
559600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
560588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
560603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.43ms 
560604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
560604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
560605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
563577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
564572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
564577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
564579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
564579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
564580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
567565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
568571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
568580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.17ms 
568581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
568581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
568582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
571536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
572527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
572530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 905.94ns 
572531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
572531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
572532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
575525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
576510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
576512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.24ns 
576514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
576514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
576517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
579527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
580502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
580510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
580512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
580513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.71ns 
580514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
583531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
584512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
584517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
584518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
584518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
584519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
587519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
588495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
588499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
588501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
588501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
588501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
591538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
592527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
592531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
592532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
592532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
592533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
595558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
596528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
596535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
596536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
596536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
596537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
599532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
600548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
600552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
600554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
600554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
600554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
603561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
604595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
604610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.56ms 
604611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
604611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
604612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
607638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
608642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
608645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 877.14ns 
608646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
608646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
608647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
611630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
612624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
612634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.63ms 
612636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
612636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
612636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
615635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
616645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
616649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
616650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
616650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
616651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
619659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
620624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
620627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
620628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
620628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
620629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
623626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
624615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
624622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
624623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
624623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
624624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
627659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
628679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
628683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
628684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
628684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
628685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
631683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
632682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
632687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
632689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
632689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.41ns 
632690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
635691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
636697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
636703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
636704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
636704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
636705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
639721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
640711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
640718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
640719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
640719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
640720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
643733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
644723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
644744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.65ms 
644746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
644746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
644746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
647770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
648773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
648795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.32ms 
648797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
648797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
648798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
651802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
652809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
652824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.85ms 
652825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
652826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
652826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
655843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
656812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
656828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.26ms 
656829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
656829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
656830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
659835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
660859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
660896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.19ms 
660898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
660898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
660899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
663934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
664955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
664991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.86ms 
664993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
664993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
664994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
668057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
669048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
669083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.3ms 
669085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
669085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
669086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
672092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
673093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
673114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.64ms 
673120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
673120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
673121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
676105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
677089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
677137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.34ms 
677139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
677139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
677140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
680131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
681120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
681191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.56ms 
681194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
681194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
681195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
684166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
685160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
685218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.66ms 
685220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
685220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
685221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
688209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
689207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
689267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.17ms 
689269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
689269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
689270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
692239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
693227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
693290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.23ms 
693291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
693291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
693293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
696275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
697275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
697447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 164.23ms 
697448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
697448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
697449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
700430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
701442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
701453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ms 
701455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
701455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
701455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
704395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
705385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
705396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.74ms 
705397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
705397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
705398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
708402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
709384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
709391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
709393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
709393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
709394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
712351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
713347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
713373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.12ms 
713375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
713375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.11ns 
713376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
716349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
717326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
717341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
717342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
717342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
717343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
720371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
721351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
721355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
721356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
721356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
721357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
724339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
725349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
725374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.51ms 
725376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
725376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
725376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
728356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
729339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
729363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.63ms 
729365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
729365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
729365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
732333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
733319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
733348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.44ms 
733351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
733351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.01ns 
733352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
736343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
737339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
737342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
737344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
737344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
737345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
740338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
741338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
741343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
741344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
741344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
741345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
744349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
745346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
745354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.09ms 
745356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
745356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
745357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
748344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
749337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
749345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.12ms 
749347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
749347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
749349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
752337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
753324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
753429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.76ms 
753430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
753430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
753431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
756495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
757487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
757526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.63ms 
757528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
757528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.91ns 
757529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
760485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
761484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
761516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.33ms 
761518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
761518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
761519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
764507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
765499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
765501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 348.41ns 
765502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
765502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
765504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
768543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
769538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
769845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 295.81ms 
769848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
769848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.41ns 
769849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
772899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
772900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
773906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
773983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.76ms 
773984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
773984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
773985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
776968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
777993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
777995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 443.72ns 
777996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
777997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
777997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
780965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
781942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
781945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 451.22ns 
781946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
781946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
781947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
784981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
785962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
785965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 497.52ns 
785966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
785966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
785967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
788966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
789944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
789946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 623.62ns 
789947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
789948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
789948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
792952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
793954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
794074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.76ms 
794076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
794076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.41ns 
794077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
797084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
797084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
798105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
798158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.06ms 
798159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
798159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
798161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
801198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
802191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
802193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 
802227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
802274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
802298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
802306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
802319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
802324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
802325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
802328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
802334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
802336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
802342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
802348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
802618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
802620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
802621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
802622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
802624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
802759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
802760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
802761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
802763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
802765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
802766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
802991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
802994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
802995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
802996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
802997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
802998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
803172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
803174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
803175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
803176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
803177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
803178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
803186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
803187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
803188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
803191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
803192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
803193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
803203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
803204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
803205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
803206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
803207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
803208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
803430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
803432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
803433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
803592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
803594     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)'' 
803597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
803599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
803601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
803602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
803603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
803604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
803608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
803610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
803611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
803612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
803613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
803750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
803755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
803757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
803759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
803760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
803761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
803762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
803948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
803950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
803951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
803953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
803954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
803955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
803955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
803957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
804123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
804125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
804238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
804243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
804249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
804250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
804251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
804252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
804253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
804255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
804255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
804257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
804266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
804272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
804396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
804398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
804399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
804400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
804401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
804402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
804403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
804404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
804472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
804480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
804593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
804595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
804597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
804599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
804600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
804601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
804752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
804757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
804759     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)'' 
804760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
804761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
804762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
804763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
804764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
804775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
804776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
804778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
804779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
804891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
804893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
804894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
804895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
804902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
804904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
805036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
805038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
805039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
805041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
805042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
805043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
805043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
805045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
805156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
805158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
805255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
805256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
805257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
805262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
805267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
805272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
805428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
805430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
805431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
805432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
805445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
805559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
810098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
810100     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)'' 
810107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
810108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
810110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
810110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
810111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
810122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
810124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
810125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
810126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
810127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
810254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
810259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
810260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
810261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
810263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
810263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
810265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
810391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
810393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
810394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
810396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
810397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
810398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
810399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
810402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
810507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
810508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
810609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
810614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
810620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
810622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
810622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
810624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
810637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
810742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
810744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
810744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
810745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
810841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
810852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
810853     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)'' 
810855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
810856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
810856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
810857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
810858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
810871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
810872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
810874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
810874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
810875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
810994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
810996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
810997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
810998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
810998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
811176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
811182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
811183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
811184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
811185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
811185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
811188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
811327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
811328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
811329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
811330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
811331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
811332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
811332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
811333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
811334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
811335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
811337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
811337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
811338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
811338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
811339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
811454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
811455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
811462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
811567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
811674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
811676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
811677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
811677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
811679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
811679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
811680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
811680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
811681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
811793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
811800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
811919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
811921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
811921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
811923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
811923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
811924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
811924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
811925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
811932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
811933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
812041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
812048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
812055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
812190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
812191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
812192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
812193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
812194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
812194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
812195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
812196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
812267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
812269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
812270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
812270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
812271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
812278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
812285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
812437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
812557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
812558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
812559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
812560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
812781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
812897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
812898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
817431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
817441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
817442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
817443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
817444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
817601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
817603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
817604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
817605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
817606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
817749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
821885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
825968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
825974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
825975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
825976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
825977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
826140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
826142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
826143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
826145     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)' ...' 
826147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
827726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
827726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
827728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
830850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
830851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
831941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
831942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
831943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
831954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
831966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
831969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
831971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
831972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
831979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
831981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
831985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
831988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
831989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
832002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
832004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
832004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
832075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
832077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
832077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
832078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
832078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
832162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
832162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
832164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
832165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
832166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
832170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
832171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
832171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
832173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
832174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
832175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
832281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
832282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
832282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
832284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
832285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
832286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
832399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
832400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
832401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
832401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
832402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
832404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
832404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
832405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
832406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
832407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
832408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
832408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
832409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
832410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
832411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
832411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
832412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
832414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
832415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
832418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
832466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
832468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
832545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
832546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
832548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
832550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
832551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
832551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
832615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
832618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
832620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
832621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
832623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
832624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
832625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
832689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
832692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
832696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
832767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
832837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
832837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.01ns 
832838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
835992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
835992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
837089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
837134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.72ms