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

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

tests
0

failures
0

ignored
10m24.47s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.020s passed
powPositiveConcrete data()[101] 3.035s passed
powGeq1Concrete data()[102] 3.012s passed
pow2InIntLower data()[103] 3.011s passed
pow2InIntUpper data()[104] 3.014s passed
logSelfConcrete data()[105] 3.025s passed
log1Concrete data()[106] 3.070s passed
logProduct data()[107] 3.022s passed
logTimesBaseConcrete data()[108] 3.017s passed
logProdIdentity data()[109] 3.030s passed
moduloByteIsInByte data()[10] 3.077s passed
logProdIdentityConcrete data()[110] 3.025s passed
logPowIdentity data()[111] 3.041s passed
logPowIdentityConcrete data()[112] 3.021s passed
logPositive data()[113] 3.029s passed
logPositiveConcrete data()[114] 3.023s passed
logMono data()[115] 3.039s passed
logMonoConcrete data()[116] 3.039s passed
powLogLess data()[117] 3.034s passed
powLogMore2 data()[118] 3.034s passed
logLessThanPow data()[119] 3.040s passed
moduloCharIsInChar data()[11] 3.183s passed
logLessThanPowConcrete data()[120] 3.042s passed
logSqueeze data()[121] 3.017s passed
ifthenelse_equals data()[122] 3.014s passed
ifthenelse_equals_1 data()[123] 3.014s passed
ifthenelse_equals_2 data()[124] 3.032s passed
disjointWithSingleton1 data()[125] 3.022s passed
disjointWithSingleton2 data()[126] 3.015s passed
disjointArrayRanges data()[127] 3.045s passed
disjointArrayRangeAllFields1 data()[128] 3.027s passed
disjointArrayRangeAllFields2 data()[129] 3.029s passed
div_unique1 data()[12] 3.273s passed
seqSelfDefinition data()[130] 3.046s passed
seqOutsideValue data()[131] 3.029s passed
castedGetAny data()[132] 3.024s passed
seqGetAlphaCast data()[133] 3.041s passed
getOfSeqSingleton data()[134] 3.034s passed
getOfSeqSingletonConcrete data()[135] 3.028s passed
getOfSeqConcat data()[136] 3.054s passed
getOfSeqSub data()[137] 3.028s passed
getOfSeqReverse data()[138] 3.043s passed
lenOfSeqEmpty data()[139] 3.020s passed
div_unique2 data()[13] 3.138s passed
lenOfSeqSingleton data()[140] 3.039s passed
lenOfSeqConcat data()[141] 3.027s passed
lenOfSeqSub data()[142] 3.043s passed
lenOfSeqReverse data()[143] 3.022s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.018s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.038s passed
getOfSeqSingletonEQ data()[146] 3.023s passed
getOfSeqConcatEQ data()[147] 3.054s passed
getOfSeqSubEQ data()[148] 3.043s passed
getOfSeqReverseEQ data()[149] 3.028s passed
div_exists data()[14] 3.256s passed
lenOfSeqEmptyEQ data()[150] 3.043s passed
lenOfSeqSingletonEQ data()[151] 3.026s passed
lenOfSeqConcatEQ data()[152] 3.038s passed
lenOfSeqSubEQ data()[153] 3.023s passed
lenOfSeqReverseEQ data()[154] 3.060s passed
getOfSeqDefEQ data()[155] 3.034s passed
lenOfSeqDefEQ data()[156] 3.029s passed
seqConcatWithSeqEmpty1 data()[157] 3.052s passed
seqConcatWithSeqEmpty2 data()[158] 3.059s passed
seqReverseOfSeqEmpty data()[159] 3.032s passed
div_one data()[15] 3.060s passed
subSeqComplete data()[160] 3.047s passed
subSeqTailR data()[161] 3.056s passed
subSeqTailL data()[162] 3.052s passed
subSeqTailEQR data()[163] 3.062s passed
subSeqTailEQL data()[164] 3.051s passed
seqDef_split data()[165] 3.048s passed
seqDef_induction_upper data()[166] 3.090s passed
seqDef_induction_upper_concrete data()[167] 3.067s passed
seqDef_induction_lower data()[168] 3.083s passed
seqDef_induction_lower_concrete data()[169] 3.080s passed
jdiv_one data()[16] 3.076s passed
seqDef_split_in_three data()[170] 3.165s passed
seqDef_empty data()[171] 3.039s passed
seqDef_one_summand data()[172] 3.042s passed
seqDef_lower_equals_upper data()[173] 3.040s passed
seqDefOfSeq data()[174] 3.049s passed
seqSelfDefinitionEQ2 data()[175] 3.047s passed
indexOfSeqSingleton data()[176] 3.040s passed
indexOfSeqConcatFirst data()[177] 3.035s passed
indexOfSeqConcatSecond data()[178] 3.050s passed
indexOfSeqSub data()[179] 3.046s passed
div_zero data()[17] 3.107s passed
lenOfArray2seq data()[180] 3.036s passed
getAnyOfArray2seq data()[181] 3.036s passed
getOfArray2seq data()[182] 3.039s passed
getAnyOfNPermInv data()[183] 3.043s passed
seqNPermRange data()[184] 3.096s passed
seqPermTrans data()[185] 3.066s passed
seqPermRefl data()[186] 3.060s passed
seqPermSplit data()[187] 3.042s passed
seqNPermRight data()[188] 3.242s passed
seqPermFromSwap data()[189] 3.102s passed
divResZero1 data()[18] 3.076s passed
seqPermTransAlt0 data()[190] 3.047s passed
seqPermTransAlt1 data()[191] 3.046s passed
seqPermTransAlt2 data()[192] 3.033s passed
seqPermTransAlt3 data()[193] 3.035s passed
seqPermForall data()[194] 3.113s passed
seqPermExists data()[195] 3.098s passed
schiffl_lemma_2 data()[196] 20.275s passed
schiffl_thm_1 data()[197] 3.847s passed
eqSameSeq data()[198] 3.158s passed
divResZero2 data()[19] 3.076s passed
eqTermCut data()[1] 3.682s passed
divResOne1 data()[20] 3.092s passed
divResOne2 data()[21] 3.110s passed
div_cancel1 data()[22] 3.084s passed
div_cancel2 data()[23] 3.051s passed
divAddMultDenom data()[24] 3.079s passed
divMinus data()[25] 3.195s passed
divMinusDenom data()[26] 3.191s passed
divLeastDPos data()[27] 3.083s passed
divLeastDNeg data()[28] 3.059s passed
divGreatestDPos data()[29] 3.048s passed
equivAllRight data()[2] 3.405s passed
divGreatestDNeg data()[30] 3.043s passed
divIncreasingPos data()[31] 3.075s passed
divIncreasingNeg data()[32] 3.047s passed
jdiv_zero data()[33] 3.039s passed
jdivPulloutMinusNum data()[34] 3.044s passed
jdivPulloutMinusDenom data()[35] 3.134s passed
jdiv_uniquePosPos data()[36] 3.081s passed
jdiv_uniquePosNeg data()[37] 3.053s passed
jdiv_uniqueNegPos data()[38] 3.048s passed
jdiv_uniqueNegNeg data()[39] 3.050s passed
irrflConcrete1 data()[3] 3.247s passed
jdivMultDenom1 data()[40] 3.071s passed
jdivMultDenom2 data()[41] 3.053s passed
mod_geZero data()[42] 3.029s passed
mod_lessDenom data()[43] 3.034s passed
jmod_NumPos data()[44] 3.032s passed
jmod_NumNeg data()[45] 3.039s passed
jmod_geZero data()[46] 3.042s passed
jmodNumZero data()[47] 3.031s passed
jmod_pulloutminusNum data()[48] 3.037s passed
jmod_pulloutminusDenom data()[49] 3.035s passed
irrflConcrete2 data()[4] 3.206s passed
jmodUnique1 data()[50] 3.084s passed
jmodUnique2 data()[51] 3.120s passed
intDivRem data()[52] 3.026s passed
jmodjmod data()[53] 3.049s passed
jmodDivisible data()[54] 3.043s passed
jmodDivisibleRep data()[55] 3.019s passed
jdivAddMultDenom data()[56] 3.186s passed
jmodAltZero data()[57] 3.059s passed
jmodAddMultDenomZero data()[58] 3.051s passed
polyDiv_zero data()[59] 3.044s passed
cancel_gtPos data()[5] 3.223s passed
polyMod_ltdivDenom data()[60] 3.024s passed
bsum_empty data()[61] 3.019s passed
bsum_induction_upper data()[62] 3.011s passed
bsum_induction_lower data()[63] 3.033s passed
bsum_num_of_bounds data()[64] 3.040s passed
bsum_num_of_bounds2 data()[65] 3.029s passed
bsum_induction_upper2 data()[66] 3.052s passed
bsum_induction_upper_concrete data()[67] 3.017s passed
bsum_induction_upper_concrete_2 data()[68] 3.021s passed
bsum_induction_upper2_concrete data()[69] 3.015s passed
cancel_gtNeg data()[6] 3.184s passed
bsum_induction_lower_concrete data()[70] 3.014s passed
bsum_induction_lower2 data()[71] 3.033s passed
bsum_induction_lower2_concrete data()[72] 3.030s passed
bsum_positive data()[73] 3.150s passed
bsum_upper_bound data()[74] 3.067s passed
bsum_lower_bound data()[75] 3.057s passed
bsum_positive_lower_bound_element data()[76] 3.090s passed
bsum_sub_same_index data()[77] 3.067s passed
bsum_less_same_index data()[78] 3.077s passed
bsum_equal_except_one_index data()[79] 3.053s passed
moduloIntIsInInt data()[7] 3.136s passed
bsum_num_of_is_max data()[80] 3.044s passed
bsum_num_of_is_max2 data()[81] 3.068s passed
bsum_num_of_is_max3 data()[82] 3.034s passed
bsum_num_of_is_max4 data()[83] 3.042s passed
bsum_num_of_lt_max data()[84] 3.049s passed
bsum_num_of_lt_max2 data()[85] 3.041s passed
bsum_num_of_lt_max3 data()[86] 3.069s passed
bsum_num_of_lt_max4 data()[87] 3.038s passed
bsum_num_of_gt0 data()[88] 3.040s passed
bsum_num_of_gt0_alt data()[89] 3.068s passed
moduloLongIsInLong data()[8] 3.143s passed
bsum_add_concrete data()[90] 3.021s passed
bprod_all_positive data()[91] 3.049s passed
bprod_split data()[92] 3.018s passed
powConcrete0 data()[93] 3.015s passed
powConcrete1 data()[94] 3.016s passed
powSplitFactor data()[95] 3.025s passed
powAdd data()[96] 3.041s passed
powMono data()[97] 3.031s passed
powMonoConcrete data()[98] 3.014s passed
powMonoConcreteRight data()[99] 3.013s passed
moduloShortIsInShort data()[9] 3.075s passed

Standard output

515        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
532        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.88ms 
717        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729        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)

1701       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1703       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1706       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1707       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2944       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7867       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.15s 
7923       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7953       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.7ns 
7965       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7965       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 548.7ns 
7969       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10684      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
10687      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11618      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11639      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.59ms 
11647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11647      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.7ns 
11649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14151      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
14152      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15037      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15051      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ms 
15054      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15054      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337ns 
15056      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17478      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
17478      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18293      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18299      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
18302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18302      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.5ns 
18304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20695      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
20695      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21506      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
21507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21507      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
21508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23883      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
23884      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24727      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.89ms 
24729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24730      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.5ns 
24730      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27092      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
27092      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27912      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.77ms 
27913      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27913      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.7ns 
27914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30258      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
30261      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31047      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.4ns 
31050      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31050      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.8ns 
31051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33401      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
33401      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34191      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 542.8ns 
34193      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34193      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.3ns 
34194      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
36499      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37267      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 537.3ns 
37268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
37269      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39592      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
39592      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40344      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 545.5ns 
40345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40345      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
40346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
42681      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
43523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
43526      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 504ns 
43529      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
43529      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323ns 
43530      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45841      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
45841      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
46701      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
46800      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.15ms 
46801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
46801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.6ns 
46802      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
49137      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
49903      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
49936      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.77ms 
49939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
49940      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 622.7ns 
49941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52234      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
52234      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
52996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
53192      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 186.78ms 
53196      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
53196      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134ns 
53197      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55511      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
55512      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
56250      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
56254      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
56256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
56256      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
56256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58566      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
58567      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
59327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
59330      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
59332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
59332      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
59333      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61628      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
61628      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
62402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
62437      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.5ms 
62439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
62439      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183ns 
62440      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64738      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
64739      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
65498      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
65513      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ms 
65514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
65514      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
65515      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67811      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
67812      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
68574      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
68589      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
68591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
68592      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
68596      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70916      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
70916      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
71661      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
71681      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17ms 
71683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
71683      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.7ns 
71684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
74006      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
74777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
74791      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.19ms 
74792      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
74792      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.9ns 
74793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77095      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
77095      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
77853      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
77875      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.15ms 
77877      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
77877      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns 
77877      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80169      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
80169      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
80924      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
80927      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
80928      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
80928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
80929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83216      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
83216      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
83969      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
84006      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.57ms 
84007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
84007      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
84008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86386      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
86386      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
87147      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
87200      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.18ms 
87202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
87202      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
87203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89591      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
89591      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
90349      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
90391      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.98ms 
90394      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
90396      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.51ms 
90398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92708      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
92710      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
93466      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
93473      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
93476      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
93477      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 645.8ns 
93478      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95766      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
95766      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
96522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
96534      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 
96535      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
96535      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
96536      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98816      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
98817      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
99570      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
99581      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.04ms 
99583      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
99584      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 810.6ns 
99585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
101884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
102616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
102624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ms 
102626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
102626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.5ns 
102627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
104939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
105691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
105699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.07ms 
105702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
105703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 857.9ns 
105704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
107987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
108740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
108747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
108749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
108750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.5ns 
108750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
111033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
111783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
111786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
111787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
111787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
111788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
114070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
114821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
114830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.72ms 
114832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
114832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.9ns 
114833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
117141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
117877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
117960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.57ms 
117969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
117969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.5ns 
117972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
120277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
121029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
121046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
121048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
121048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.9ns 
121049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
123326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
124078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
124099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.57ms 
124101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
124101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.3ns 
124102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
126381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
127130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
127147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.01ms 
127148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
127148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
127149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
129427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
130182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
130198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.17ms 
130199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
130199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
130200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
132495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
133229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
133268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.07ms 
133270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
133270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.3ns 
133271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
135568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
136319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
136321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 987.39ns 
136322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
136322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
136323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
138594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
139345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
139350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
139352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
139352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.8ns 
139353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
141626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
142377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
142384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.24ms 
142385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
142385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
142386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
144656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
145409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
145416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
145417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
145417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
145418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
147708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
148439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
148456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ms 
148457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
148457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
148458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
150741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
151489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
151497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 
151499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
151499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
151499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
153770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
154526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
154529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
154531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
154531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.5ns 
154532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
156813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
157562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
157566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
157567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
157567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
157568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
159843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
160597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
160600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
160602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
160602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
160602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
162891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
163620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
163684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.21ms 
163686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
163687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.9ns 
163688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
165974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
166731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
166804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.1ms 
166805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
166806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
166806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
169080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
169827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
169830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
169832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
169833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.6ns 
169834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
172099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
172846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
172879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.16ms 
172881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
172881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.3ns 
172882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
175147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
175894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
175922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.93ms 
175923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
175924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
175924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
178210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
178939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
178941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
178942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
178943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
178944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
181233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
181986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
182126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 129.99ms 
182129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
182129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.8ns 
182130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
184419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
185173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
185186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.71ms 
185189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
185189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253ns 
185190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
187482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
188230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
188237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
188238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
188239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
188239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
190503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
191253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
191281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.56ms 
191283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
191283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
191284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
193566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
194292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
194303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.16ms 
194307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
194307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
194308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
196579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
197322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
197325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
197326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
197326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
197327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
199586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
200332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
200337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
200338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
200338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
200339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
202602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
203348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
203369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.24ms 
203370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
203371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
203371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
205642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
206395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
206410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.32ms 
206411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
206411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
206412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
208697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
209425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
209439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.62ms 
209440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
209440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
209441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
211739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
212488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
212491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
212492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
212492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
212493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
214755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
215503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
215507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
215508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
215508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
215509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
217774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
218523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
218528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
218529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
218529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
218530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
220794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
221540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
221543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
221544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
221544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
221545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
223828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
224555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
224557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.4ns 
224558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
224558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
224559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
226839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
227587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
227591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
227592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
227592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
227593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
229861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
230618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
230620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 918.7ns 
230621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
230622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
230622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
232958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
233707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
233768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.34ms 
233772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
233772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
233773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
236046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
236797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
236837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.35ms 
236839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
236839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.2ns 
236840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
239135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
239862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
239894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.71ms 
239895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
239896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
239896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
242190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
242938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
242985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.98ms 
242986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
242986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.3ns 
242987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
245275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
246023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
246051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.85ms 
246052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
246053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
246053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
248318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
249079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
249128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.87ms 
249129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
249129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
249130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
251406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
252153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
252181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.59ms 
252183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
252184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.3ns 
252185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
254478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
255206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
255225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.43ms 
255226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
255226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
255227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
257524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
258270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
258293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.95ms 
258294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
258294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
258295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
260562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
261309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
261328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.42ms 
261329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
261329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
261330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
263595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
264343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
264369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.35ms 
264370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
264371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
264371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
266643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
267395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
267419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.06ms 
267420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
267421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193ns 
267421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
269708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
270435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
270459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.57ms 
270461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
270461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
270462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
272759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
273505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
273528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.8ms 
273529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
273529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
273530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
275798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
276546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
276566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.06ms 
276568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
276568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.7ns 
276569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
278834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
279581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
279607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.58ms 
279608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
279608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.9ns 
279609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
281899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
282651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
282674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.42ms 
282676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
282676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
282676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
284962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
285689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
285696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
285697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
285697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
285698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
287980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
288728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
288745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms 
288746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
288746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
288747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
291011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
291759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
291762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
291764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
291764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.3ns 
291765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
294029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
294775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
294778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 548.3ns 
294779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
294779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
294779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
297043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
297792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
297794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 666ns 
297795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
297795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
297796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
300083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
300812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
300819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
300820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
300820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
300821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
303105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
303854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
303860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
303861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
303862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.5ns 
303862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
306129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
306879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
306890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 
306892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
306892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.8ns 
306892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
309154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
309902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
309905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
309906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
309906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
309907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
312167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
312915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
312917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 503.9ns 
312918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
312919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
312919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
315204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
315932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
315938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
315939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
315939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
315940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
318223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
318970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
318972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 604.3ns 
318973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
318973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
318974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
321234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
321982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
321984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 516.1ns 
321985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
321985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
321986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
324246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
324993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
324995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 538.6ns 
324996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
324996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
324997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
327259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
328007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
328010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
328011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
328011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
328012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
330296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
331026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
331034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.39ms 
331035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
331035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
331036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
333353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
334101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
334104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
334105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
334105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
334106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
336372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
337120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
337126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
337127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
337127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
337128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
339392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
340140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
340144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
340145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
340145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
340146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
342413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
343159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
343173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.83ms 
343174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
343174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
343175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
345466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
346195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
346198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
346199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
346199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
346200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
348486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
349237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
349240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
349241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
349241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
349241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
351505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
352257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
352261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
352262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
352262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
352262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
354526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
355273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
355289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.73ms 
355290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
355290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
355291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
357557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
358307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
358311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 488.3ns 
358314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
358314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.6ns 
358315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
360587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
361315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
361351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.13ms 
361353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
361353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
361353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
363634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
364387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
364390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
364391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
364391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
364392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
366658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
367405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
367425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.64ms 
367426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
367426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
367427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
369690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
370436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
370458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.58ms 
370460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
370460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
370460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
372729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
373476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
373498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.73ms 
373500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
373500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
373500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
375786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
376538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
376540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 516.4ns 
376541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
376541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
376542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
378806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
379553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
379558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
379559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
379559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
379560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
381819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
382569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
382572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
382573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
382573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
382574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
384854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
385583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
385585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 839.8ns 
385586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
385586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
385587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
387865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
388615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
388618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.6ns 
388619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
388619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
388619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
390884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
391637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
391640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
391641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
391641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
391641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
393901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
394652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
394654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
394655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
394655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
394656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
396935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
397690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
397699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.21ms 
397701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
397701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
397702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
399964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
400715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
400727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.26ms 
400728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
400728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
400729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
402991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
403745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
403756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.46ms 
403757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
403757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
403757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
406034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
406790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
406801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
406803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
406803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.1ns 
406804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
409068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
409826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
409830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
409831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
409831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
409832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
412092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
412849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
412854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
412855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
412855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
412856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
415138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
415894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
415896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 660.9ns 
415897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
415897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
415897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
418162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
418919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
418926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 
418931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
418931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.8ns 
418931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
421218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
421955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
421957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 849.8ns 
421958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
421958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
421959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
424243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
425000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
425011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.46ms 
425012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
425012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
425013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
427274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
428035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
428040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
428041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
428041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
428042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
430320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
431075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
431082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
431084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
431084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159ns 
431085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
433347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
434101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
434102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.6ns 
434103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
434103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
434104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
436384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
437139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
437141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595ns 
437142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
437142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
437143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
439408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
440165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
440169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
440170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
440170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
440170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
442449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
443208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
443211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
443212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
443212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.5ns 
443213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
445477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
446231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
446233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
446235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
446235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
446235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
448512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
449249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
449252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
449253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
449253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
449254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
451530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
452284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
452289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
452290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
452290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
452291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
454573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
455310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
455313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
455314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
455314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
455315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
457602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
458356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
458366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ms 
458367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
458367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
458368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
460647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
461407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
461409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686.8ns 
461410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
461411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
461411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
463675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
464431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
464438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
464439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
464439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
464439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
466721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
467477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
467479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 830.5ns 
467481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
467481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
467482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
469750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
470504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
470506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.9ns 
470507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
470507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
470508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
472783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
473540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
473544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
473545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
473546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.5ns 
473546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
475824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
476564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
476567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
476568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
476568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
476569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
478850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
479622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
479628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
479629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
479629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
479630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
481903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
482658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
482661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
482662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
482662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
482663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
484929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
485685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
485691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
485692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
485692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
485693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
487972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
488728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
488742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.29ms 
488743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
488743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
488744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
491025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
491763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
491801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.94ms 
491803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
491803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
491803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
494068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
494824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
494834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.94ms 
494835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
494835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
494836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
497115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
497871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
497881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.29ms 
497882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
497882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
497883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
500158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
500912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
500936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.04ms 
500937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
500937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
500938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
503203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
503964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
503988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.05ms 
503989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
503989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
503990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
506272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
507028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
507050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.06ms 
507051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
507051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
507052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
509331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
510088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
510101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.53ms 
510102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
510102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
510103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
512383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
513120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
513149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.5ms 
513150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
513150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
513151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
515434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
516190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
516239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.58ms 
516240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
516240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
516241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
518517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
519271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
519307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.75ms 
519308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
519308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
519308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
521587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
522345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
522389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.1ms 
522390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
522390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
522391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
524672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
525428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
525470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.48ms 
525471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
525471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
525472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
527753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
528491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
528634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 135.44ms 
528635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
528635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
528636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
530903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
531662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
531672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.32ms 
531675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
531675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.4ns 
531676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
533953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
534708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
534715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
534716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
534716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
534717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
536995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
537751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
537756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
537757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
537757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
537758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
540034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
540788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
540805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.69ms 
540806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
540806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
540806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
543082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
543841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
543852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
543853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
543853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
543853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
546133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
546888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
546891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
546892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
546892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
546893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
549174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
549910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
549926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.83ms 
549927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
549927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
549928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
552206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
552961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
552977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ms 
552978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
552978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
552978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
555250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
556005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
556023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.18ms 
556024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
556024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns 
556024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
558300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
559056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
559058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
559059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
559059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.8ns 
559060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
561335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
562091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
562095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
562096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
562096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
562097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
564371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
565128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
565133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
565134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
565134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
565135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
567414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
568170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
568176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
568177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
568177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.1ns 
568178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
570450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
571205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
571272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.18ms 
571273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
571273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
571274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
573552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
574311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
574338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.24ms 
574340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
574340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
574340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
576622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
577378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
577399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.78ms 
577400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
577400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
577401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
579681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
580439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
580440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 270.2ns 
580442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
580442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.8ns 
580443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
582734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
583491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
583682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 180.53ms 
583684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
583684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
583684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
585975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
586737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
586784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.03ms 
586785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
586785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
586786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
589091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
589829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
589831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 288.9ns 
589832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
589832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
589833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
592120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
592876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
592877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 306.9ns 
592879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
592879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
592879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
595152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
595909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
595910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 303.4ns 
595911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
595911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.6ns 
595912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
598187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
598944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
598945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 465.7ns 
598946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
598947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
598947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
601219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
601973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
602058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.27ms 
602060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
602060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.1ns 
602061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
604350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
605109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
605157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.54ms 
605158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
605158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
605159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
607453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
608210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
608211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
608234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
608265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
608281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
608284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
608295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
608300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
608310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
608313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
608318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
608320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
608324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
608326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
608548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
608550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
608551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
608553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
608554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
608675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
608676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
608679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
608681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
608682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
608684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
608854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
608856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
608857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
608858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
608859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
608862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
608966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
608968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
608969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
608970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
608971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
608972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
608979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
608980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
608980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
608983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
608987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
608988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
608996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
608997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
608998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
608999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
609000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
609001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
609116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
609117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
609119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
609214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
609215     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)'' 
609217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
609218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
609220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
609221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
609222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
609223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
609229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
609235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
609237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
609237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
609238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
609339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
609342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
609344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
609344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
609345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
609346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
609347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
609471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
609473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
609474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
609475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
609476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
609477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
609477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
609478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
609549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
609551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
609635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
609638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
609642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
609643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
609644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
609645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
609645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
609646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
609646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
609647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
609654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
609658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
609761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
609762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
609763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
609764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
609765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
609765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
609766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
609767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
609811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
609815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
609888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
609890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
609892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
609893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
609894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
609895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
610000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
610003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
610006     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)'' 
610008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
610009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
610012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
610013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
610014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
610021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
610030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
610031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
610032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
610109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
610111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
610111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
610112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
610113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
610114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
610200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
610201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
610202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
610204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
610204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
610205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
610205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
610206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
610275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
610276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
610340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
610340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
610341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
610345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
610348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
610352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
610456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
610457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
610458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
610459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
610467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
610539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
613710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
613711     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)'' 
613716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
613717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
613718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
613718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
613719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
613726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
613727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
613728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
613729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
613729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
613813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
613816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
613817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
613818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
613819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
613819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
613820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
613905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
613906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
613907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
613908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
613909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
613909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
613910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
613911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
613979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
613980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
614045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
614049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
614052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
614053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
614054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
614054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
614063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
614134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
614135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
614135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
614136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
614201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
614209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
614210     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)'' 
614211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
614212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
614213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
614213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
614213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
614223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
614224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
614225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
614225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
614226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
614307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
614309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
614311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
614312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
614313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
614401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
614406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
614407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
614408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
614408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
614409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
614410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
614503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
614505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
614506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
614507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
614508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
614511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
614513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
614514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
614514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
614515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
614516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
614516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
614517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
614517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
614518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
614597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
614598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
614603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
614674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
614748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
614749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
614750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
614751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
614752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
614752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
614752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
614753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
614753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
614870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
614875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
614955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
614957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
614957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
614959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
614959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
614959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
614959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
614960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
614965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
614966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
615038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
615042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
615047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
615138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
615139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
615140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
615141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
615141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
615141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
615142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
615143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
615193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
615194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
615194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
615195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
615196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
615200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
615205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
615311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
615390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
615391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
615392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
615394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
615545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
615624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
615625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
618406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
618411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
618412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
618412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
618413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
618516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
618517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
618518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
618519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
618519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
618615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
621385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
624249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
624253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
624254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
624255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
624255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
624358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
624359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
624360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
624361     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)' ...' 
624363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
625432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
625432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
625433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
627821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
628601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
628603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ns 
628603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
628611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
628622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
628625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
628626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
628627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
628631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
628633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
628636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
628638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
628639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
628648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
628649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
628650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
628696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
628697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
628698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
628699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
628699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
628768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
628768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
628770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
628770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
628771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
628775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
628775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
628776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
628777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
628778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
628778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
628860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
628861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
628862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
628863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
628864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
628864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
628949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
628950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
628950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
628951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
628952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
628953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
628953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
628953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
628954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
628955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
628955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
628956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
628956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
628957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
628957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
628957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
628958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
628959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
628960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
628962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
628997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
628998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
629055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
629056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
629058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
629059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
629059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
629060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
629111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
629113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
629114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
629116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
629117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
629118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
629118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
629169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
629171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
629174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
629226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
629280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
629280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.4ns 
629281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
631612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
632407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
632437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.61ms