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

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

tests
0

failures
0

ignored
10m27.38s

duration
100%

successful

Tests

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

Standard output

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

1798       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1803       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1804       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1805       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3365       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8622       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.8s 
8700       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8735       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.8ns 
8750       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8751       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199ns 
8756       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11455      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
11457      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12360      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12387      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ms 
12404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12404      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.9ns 
12406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14944      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
14944      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15764      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
15767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15767      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.8ns 
15768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18234      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
18236      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19091      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19097      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms 
19100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19100      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.3ns 
19101      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
21499      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22295      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
22298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22298      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.6ns 
22299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
24651      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25550      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.01ms 
25555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25555      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 561.1ns 
25557      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27909      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
27910      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28715      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.23ms 
28718      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28719      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347ns 
28720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
31045      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31822      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 710.1ns 
31824      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31825      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310ns 
31826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34163      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
34163      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34924      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 631.1ns 
34927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34927      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.1ns 
34928      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37271      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
37271      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38029      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.8ns 
38032      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38032      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.7ns 
38033      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
40377      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41140      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.4ns 
41144      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41144      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.6ns 
41146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43505      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
43505      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44264      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618ns 
44267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.3ns 
44269      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46579      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
46579      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47354      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47390      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.66ms 
47391      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47391      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.5ns 
47392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49733      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
49733      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50515      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.1ms 
50517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50517      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.3ns 
50519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52880      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
52881      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
53831      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 166.57ms 
53835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
53835      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.4ns 
53836      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56196      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
56196      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
56937      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
56944      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
56947      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
56948      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 622.8ns 
56949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
59300      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60053      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60057      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
60060      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60060      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.3ns 
60062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62406      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
62407      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63138      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63172      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.14ms 
63175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63175      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.6ns 
63176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65530      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
65531      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66278      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66290      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 
66291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66291      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
66292      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
68601      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69367      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
69369      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69369      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.8ns 
69370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71697      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
71697      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
72455      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
72468      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.65ms 
72471      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
72471      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 477.8ns 
72474      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74821      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
74821      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
75586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
75599      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
75601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
75601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.9ns 
75602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77927      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
77928      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
78674      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
78691      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.55ms 
78692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
78692      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.1ns 
78693      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81003      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
81003      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
81752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
81755      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
81756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
81757      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
81757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84083      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
84085      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
84812      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
84843      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.79ms 
84846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
84846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.3ns 
84847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
87174      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
87920      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
87963      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.8ms 
87966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
87967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.4ns 
87968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90307      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
90308      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91064      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.8ms 
91068      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91069      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.55ms 
91071      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93409      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
93410      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94160      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
94162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94163      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.9ns 
94164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96474      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
96474      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
97240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
97251      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.29ms 
97253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
97253      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.8ns 
97254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99575      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
99575      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
100319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
100329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.92ms 
100330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
100330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.4ns 
100331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
102648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
103397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
103403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
103405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
103405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.3ns 
103406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
105729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
106481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
106487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
106490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
106491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.38ms 
106492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
108814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
109558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
109564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
109565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
109565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
109566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
111897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
112622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
112625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
112626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
112626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
112627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
114956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
115700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
115709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.38ms 
115710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
115710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
115711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
118021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
118765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
118796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.89ms 
118799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
118800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1ms 
118801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
121174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
121915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
121929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.87ms 
121930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
121930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
121931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
124254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
125016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
125030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.99ms 
125032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
125033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.1ns 
125034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
127366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
128109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
128124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ms 
128126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
128126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.4ns 
128127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
130432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
131175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
131191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.51ms 
131193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
131193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.3ns 
131194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
133521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
134243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
134274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.48ms 
134276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
134276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.9ns 
134277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
136612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
137355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
137361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
137363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
137363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
137364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
139702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
140425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
140428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
140430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
140430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.1ns 
140431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
142752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
143494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
143501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms 
143502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
143502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
143503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
145810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
146552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
146559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.97ms 
146561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
146561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
146561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
148888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
149630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
149646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.09ms 
149647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
149647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146ns 
149648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
151948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
152707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
152714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
152715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
152715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
152716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
155040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
155786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
155790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
155792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
155792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.9ns 
155793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
158095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
158837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
158841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
158842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
158842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.5ns 
158843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
161164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
161886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
161889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
161891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
161891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.7ns 
161892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
164222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
164968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
165026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.33ms 
165028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
165028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.1ns 
165029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
167322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
168065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
168131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.94ms 
168134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
168134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.8ns 
168135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
170443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
171191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
171194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
171195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
171195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
171196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
173484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
174224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
174276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.43ms 
174279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
174284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.97ms 
174285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
176599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
177337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
177358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.18ms 
177360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
177360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.6ns 
177361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
179658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
180399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
180402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
180403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
180403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
180404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
182713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
183464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
183563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.23ms 
183566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
183566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.7ns 
183567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
185854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
186592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
186600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.62ms 
186602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
186602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
186602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
188919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
189639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
189645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
189648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
189648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.5ns 
189649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
191962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
192699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
192713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.12ms 
192714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
192714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
192715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
195018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
195736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
195749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.44ms 
195751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
195751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
195752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
198041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
198774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
198777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
198779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
198779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
198780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
201068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
201808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
201811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
201812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
201813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
201813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
204119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
204859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
204873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ms 
204874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
204874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
204875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
207163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
207902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
207913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.06ms 
207915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
207915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
207915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
210214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
210932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
210944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.87ms 
210945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
210945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
210946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
213251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
213990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
213993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 922.69ns 
213994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
213994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
213995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
216295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
217014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
217017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
217018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
217018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
217019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
219314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
220051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
220055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.66ms 
220056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
220056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
220057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
222336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
223083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
223086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 863ns 
223087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
223088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
223088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
225391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
226128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
226130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 478.5ns 
226131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
226131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
226132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
228418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
229155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
229158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
229159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
229159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
229160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
231462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
232201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
232203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717ns 
232205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
232205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227ns 
232206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
234494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
235232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
235269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.82ms 
235271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
235271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
235272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
237578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
238298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
238323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.01ms 
238324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
238324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
238325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
240644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
241390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
241409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ms 
241410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
241411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
241411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
243696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
244434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
244459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.17ms 
244460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
244460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
244461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
246756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
247497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
247513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.02ms 
247514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
247514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
247515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
249801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
250539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
250570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.26ms 
250571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
250572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.1ns 
250572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
252882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
253619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
253635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.94ms 
253636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
253636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
253637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
255920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
256660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
256672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.01ms 
256674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
256674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
256674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
258969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
259708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
259722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.47ms 
259723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
259723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
259724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
262003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
262742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
262755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ms 
262756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
262756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
262757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
265056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
265776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
265792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.41ms 
265793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
265793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
265794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
268094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
268834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
268850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ms 
268851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
268852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.1ns 
268853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
271137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
271875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
271891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.82ms 
271892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
271892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
271893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
274204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
274942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
274957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.99ms 
274958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
274958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
274959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
277237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
277977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
277990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.71ms 
277991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
277991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
277992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
280290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
281026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
281041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.65ms 
281043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
281043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
281043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
283331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
284070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
284100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.29ms 
284101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
284101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
284102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
286394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
287137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
287143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
287144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
287144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
287144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
289424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
290163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
290174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms 
290175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
290175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
290176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
292477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
293196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
293199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
293200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
293201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
293201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
295502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
296239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
296241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573ns 
296242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
296243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
296243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
298516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
299255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
299257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.8ns 
299258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
299258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
299259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
301552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
302288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
302294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
302296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
302296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
302296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
304573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
305312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
305317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
305319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
305319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.8ns 
305320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
307613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
308353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
308364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
308365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
308366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.2ns 
308366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
310643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
311383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
311385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
311387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
311387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
311387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
313675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
314394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
314396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 400.2ns 
314397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
314397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
314398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
316692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
317431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
317437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
317439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
317439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.2ns 
317440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
319732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
320450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
320452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 467.6ns 
320453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
320453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
320454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
322745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
323486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
323488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 457.4ns 
323489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
323489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
323490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
325764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
326501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
326503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 464.3ns 
326504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
326504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
326505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
328793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
329535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
329539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
329540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
329540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
329541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
331829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
332571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
332577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
332579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
332579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
332579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
334874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
335610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
335613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
335614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
335614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
335615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
337895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
338635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
338640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
338641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
338641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
338642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
340938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
341676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
341680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
341681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
341681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
341682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
343964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
344704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
344715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
344717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
344717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
344717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
347009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
347749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
347752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
347754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
347754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
347754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
350029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
350770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
350773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 917.1ns 
350774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
350774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
350775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
353073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
353811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
353814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
353815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
353815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
353816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
356087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
356824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
356837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.81ms 
356839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
356839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.5ns 
356840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
359134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
359871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
359875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 321.5ns 
359877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
359877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
359877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
362165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
362886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
362911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.35ms 
362912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
362912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
362913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
365204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
365941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
365944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
365945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
365945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
365945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
368236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
368973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
368987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.69ms 
368988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
368988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
368989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
371266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
372003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
372016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ms 
372017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
372017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
372018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
374306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
375042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
375059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.09ms 
375060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
375061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
375061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
377366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
378103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
378105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 455.6ns 
378106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
378106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
378107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
380380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
381120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
381124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
381126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
381126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
381126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
383417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
384158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
384162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
384164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
384164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.7ns 
384165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
386459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
387200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
387203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 671.3ns 
387204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
387204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
387204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
389489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
390230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
390232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 639.3ns 
390233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
390233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
390233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
392524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
393267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
393270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
393271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
393271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
393272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
395559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
396302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
396304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 954.13ns 
396306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
396306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.4ns 
396307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
398581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
399324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
399331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.31ms 
399333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
399333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
399333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
401633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
402376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
402382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
402383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
402383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
402384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
404681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
405425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
405431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.27ms 
405432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
405432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
405432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
407733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
408481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
408489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
408490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
408490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
408490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
410769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
411516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
411525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
411527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
411527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.91ns 
411528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
413819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
414564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
414567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
414568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
414569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
414569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
416864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
417609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
417611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 597.51ns 
417612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
417612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
417613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
419907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
420653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
420655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 816.41ns 
420657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
420657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
420657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
422971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
423718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
423720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 797.81ns 
423721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
423722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
423722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
426016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
426743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
426751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
426752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
426752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
426753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
429042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
429789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
429791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
429792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
429792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
429793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
432091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
432837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
432842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
432843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
432843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
432843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
435136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
435885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
435887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717.21ns 
435889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
435889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
435889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
438183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
438928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
438930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.11ns 
438931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
438931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
438931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
441224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
441969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
441972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
441973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
441973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
441974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
444269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
445016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
445019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811.61ns 
445020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
445020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
445020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
447318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
448065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
448067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 936.61ns 
448068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
448068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
448069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
450364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
451112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
451114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.21ns 
451116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
451116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
451116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
453417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
454166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
454169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
454171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
454171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
454171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
456475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
457221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
457224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 803.81ns 
457225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
457225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
457225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
459538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
460286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
460293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.99ms 
460295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
460295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
460295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
462597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
463343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
463345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 448ns 
463346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
463346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
463347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
465655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
466404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
466409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
466410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
466410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
466411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
468704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
469449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
469451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.9ns 
469452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
469453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
469453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
471747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
472493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
472498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 569.11ns 
472499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
472499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
472500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
474792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
475537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
475540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
475542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
475542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
475542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
477844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
478593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
478596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 868.51ns 
478597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
478597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.7ns 
478598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
480896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
481648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
481651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
481652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
481652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
481653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
483952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
484699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
484702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
484703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
484703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
484703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
487001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
487747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
487751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
487752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
487752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
487753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
490042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
490804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
490811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
490812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
490812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
490813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
493103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
493849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
493857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.37ms 
493858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
493858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
493858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
496169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
496897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
496902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
496903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
496903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
496923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
499227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
499975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
499981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
499982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
499982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
499983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
502279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
503032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
503043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.13ms 
503044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
503044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
503045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
505342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
506089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
506098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.34ms 
506100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
506100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
506100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
508391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
509137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
509146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ms 
509147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
509147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
509148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
511461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
512208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
512214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
512216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
512216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
512216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
514514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
515262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
515281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.43ms 
515282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
515282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
515283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
517581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
518329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
518349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.58ms 
518351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
518351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
518351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
520646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
521393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
521411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.03ms 
521412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
521412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
521413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
523726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
524473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
524493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.73ms 
524495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
524495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.9ns 
524496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
526789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
527537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
527555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.98ms 
527556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
527556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
527557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
529847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
530593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
530638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.65ms 
530639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
530639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
530640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
532952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
533699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
533703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
533704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
533704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
533705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
536000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
536749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
536753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
536755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
536755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
536755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
539046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
539817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
539822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
539823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
539824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.2ns 
539824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
542119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
542865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
542877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ms 
542878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
542878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
542878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
545168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
545918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
545924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
545925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
545926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
545926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
548232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
548977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
548980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
548981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
548981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
548981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
551266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
552013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
552022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.28ms 
552023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
552023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
552024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
554337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
555083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
555092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.46ms 
555094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
555094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
555094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
557389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
558134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
558146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.07ms 
558148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
558148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
558148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
560463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
561209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
561211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 893.21ns 
561212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
561213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
561213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
563512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
564259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
564262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
564264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
564264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
564264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
566572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
567318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
567323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
567325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
567325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
567325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
569621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
570367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
570371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
570372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
570372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
570373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
572684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
573433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
573472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.95ms 
573474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
573474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
573474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
575798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
576548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
576566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.19ms 
576567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
576568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.2ns 
576568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
578888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
579636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
579646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.45ms 
579648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
579648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
579648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
581963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
582709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
582711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 151.2ns 
582712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
582712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
582713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
585021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
585767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
585842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.25ms 
585844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
585844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
585845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
588156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
588905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
588937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.23ms 
588938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
588938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
588939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
591253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
592000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
592002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 282.8ns 
592005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
592005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.2ns 
592005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
594310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
595064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
595068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 201.5ns 
595069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
595069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
595070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
597378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
598128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
598130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 199.8ns 
598131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
598131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
598131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
600452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
601208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
601210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 312.8ns 
601211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
601211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
601212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
603543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
604340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
604493     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
604501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 156.86ms 
604511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
604512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.2ns 
604512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
606857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
607607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
607658     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
607659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.81ms 
607660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
607660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
607661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
610000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
610764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
610766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ns 
610789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
610825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
610837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
610842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
610852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
610853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
610856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
610857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
610861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
610862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
610864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
610866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
611099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
611101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
611102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
611103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
611105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
611259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
611260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
611263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
611264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
611266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
611268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
611470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
611472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
611474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
611474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
611476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
611480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
611634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
611635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
611637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
611638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
611638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
611640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
611649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
611650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
611651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
611653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
611655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
611657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
611666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
611667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
611668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
611669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
611670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
611671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
611825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
611826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
611828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
611962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
611963     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)'' 
611964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
611967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
611968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
611969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
611970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
611972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
611976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
611977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
611979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
611980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
611981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
612094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
612098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
612099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
612100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
612101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
612102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
612104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
612238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
612239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
612240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
612242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
612243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
612244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
612245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
612246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
612354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
612355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
612453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
612458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
612464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
612465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
612469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
612471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
612472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
612473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
612473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
612474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
612484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
612489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
612601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
612602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
612604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
612605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
612606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
612606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
612607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
612607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
612662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
612670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
612772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
612773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
612775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
612776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
612777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
612778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
612932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
612938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
612940     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)'' 
612942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
612943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
612944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
612945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
612946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
612958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
612962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
612964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
612965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
613091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
613092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
613093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
613095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
613095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
613096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
613215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
613216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
613217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
613219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
613220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
613220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
613221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
613221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
613308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
613309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
613387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
613388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
613388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
613393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
613396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
613401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
613584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
613585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
613586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
613588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
613601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
613688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
616990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
616992     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)'' 
617001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
617003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
617003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
617015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
617016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
617025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
617026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
617027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
617028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
617029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
617117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
617120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
617122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
617123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
617123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
617124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
617125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
617253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
617254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
617256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
617258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
617259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
617259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
617261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
617261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
617345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
617346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
617428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
617432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
617436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
617437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
617438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
617439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
617451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
617533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
617534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
617535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
617537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
617608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
617619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
617620     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)'' 
617620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
617622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
617622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
617623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
617623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
617634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
617634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
617636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
617637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
617638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
617720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
617722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
617723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
617725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
617726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
617816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
617820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
617821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
617821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
617822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
617822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
617823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
617915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
617916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
617917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
617918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
617918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
617919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
617919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
617920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
617920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
617921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
617925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
617926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
617927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
617927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
617928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
618014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
618015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
618021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
618094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
618170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
618171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
618172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
618173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
618174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
618174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
618175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
618175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
618175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
618259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
618265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
618350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
618351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
618351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
618352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
618353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
618353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
618353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
618354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
618359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
618359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
618435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
618440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
618445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
618539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
618540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
618541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
618541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
618542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
618542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
618542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
618543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
618598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
618599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
618600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
618600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
618601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
618607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
618612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
618724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
618844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
618845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
618845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
618846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
619003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
619086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
619087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
621940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
621944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
621945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
621946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
621947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
622056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
622056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
622057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
622058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
622059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
622159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
624947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
627913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
627917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
627918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
627919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
627920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
628068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
628068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
628069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
628070     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)' ...' 
628071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
629133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
629133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
629134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
631532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
632298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
632300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
632300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
632306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
632314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
632317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
632319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
632320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
632324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
632325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
632328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
632329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
632331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
632339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
632339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
632341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
632381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
632381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
632382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
632382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
632383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
632443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
632443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
632443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
632444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
632445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
632448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
632449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
632449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
632449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
632450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
632451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
632527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
632527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
632528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
632528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
632529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
632530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
632615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
632616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
632616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
632617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
632617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
632618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
632618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
632618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
632619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
632619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
632620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
632620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
632620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
632620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
632621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
632621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
632621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
632622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
632622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
632625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
632663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
632664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
632731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
632732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
632733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
632734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
632735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
632735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
632786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
632788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
632789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
632789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
632791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
632792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
632792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
632842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
632845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
632847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
632895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
632945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
632945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
632945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
635338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
636130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
636145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.59ms