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

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

tests
0

failures
0

ignored
12m51.70s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.706s passed
powPositiveConcrete data()[101] 3.657s passed
powGeq1Concrete data()[102] 3.768s passed
pow2InIntLower data()[103] 3.744s passed
pow2InIntUpper data()[104] 3.680s passed
logSelfConcrete data()[105] 3.708s passed
log1Concrete data()[106] 3.695s passed
logProduct data()[107] 3.706s passed
logTimesBaseConcrete data()[108] 3.776s passed
logProdIdentity data()[109] 3.821s passed
moduloByteIsInByte data()[10] 3.802s passed
logProdIdentityConcrete data()[110] 3.855s passed
logPowIdentity data()[111] 3.677s passed
logPowIdentityConcrete data()[112] 3.662s passed
logPositive data()[113] 3.681s passed
logPositiveConcrete data()[114] 3.704s passed
logMono data()[115] 3.833s passed
logMonoConcrete data()[116] 3.820s passed
powLogLess data()[117] 3.846s passed
powLogMore2 data()[118] 3.841s passed
logLessThanPow data()[119] 3.779s passed
moduloCharIsInChar data()[11] 3.715s passed
logLessThanPowConcrete data()[120] 3.689s passed
logSqueeze data()[121] 3.754s passed
ifthenelse_equals data()[122] 3.845s passed
ifthenelse_equals_1 data()[123] 3.722s passed
ifthenelse_equals_2 data()[124] 3.880s passed
disjointWithSingleton1 data()[125] 3.816s passed
disjointWithSingleton2 data()[126] 3.744s passed
disjointArrayRanges data()[127] 3.729s passed
disjointArrayRangeAllFields1 data()[128] 3.716s passed
disjointArrayRangeAllFields2 data()[129] 3.794s passed
div_unique1 data()[12] 3.758s passed
seqSelfDefinition data()[130] 3.901s passed
seqOutsideValue data()[131] 3.793s passed
castedGetAny data()[132] 3.895s passed
seqGetAlphaCast data()[133] 3.814s passed
getOfSeqSingleton data()[134] 3.744s passed
getOfSeqSingletonConcrete data()[135] 3.730s passed
getOfSeqConcat data()[136] 3.803s passed
getOfSeqSub data()[137] 3.753s passed
getOfSeqReverse data()[138] 3.749s passed
lenOfSeqEmpty data()[139] 3.697s passed
div_unique2 data()[13] 3.800s passed
lenOfSeqSingleton data()[140] 3.789s passed
lenOfSeqConcat data()[141] 3.797s passed
lenOfSeqSub data()[142] 3.716s passed
lenOfSeqReverse data()[143] 3.818s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.726s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.774s passed
getOfSeqSingletonEQ data()[146] 3.700s passed
getOfSeqConcatEQ data()[147] 3.730s passed
getOfSeqSubEQ data()[148] 3.722s passed
getOfSeqReverseEQ data()[149] 3.781s passed
div_exists data()[14] 4.092s passed
lenOfSeqEmptyEQ data()[150] 3.696s passed
lenOfSeqSingletonEQ data()[151] 3.744s passed
lenOfSeqConcatEQ data()[152] 3.714s passed
lenOfSeqSubEQ data()[153] 3.710s passed
lenOfSeqReverseEQ data()[154] 3.737s passed
getOfSeqDefEQ data()[155] 3.671s passed
lenOfSeqDefEQ data()[156] 3.763s passed
seqConcatWithSeqEmpty1 data()[157] 3.765s passed
seqConcatWithSeqEmpty2 data()[158] 3.807s passed
seqReverseOfSeqEmpty data()[159] 3.899s passed
div_one data()[15] 3.729s passed
subSeqComplete data()[160] 3.753s passed
subSeqTailR data()[161] 3.739s passed
subSeqTailL data()[162] 3.694s passed
subSeqTailEQR data()[163] 3.680s passed
subSeqTailEQL data()[164] 3.712s passed
seqDef_split data()[165] 3.726s passed
seqDef_induction_upper data()[166] 3.906s passed
seqDef_induction_upper_concrete data()[167] 3.766s passed
seqDef_induction_lower data()[168] 3.814s passed
seqDef_induction_lower_concrete data()[169] 3.755s passed
jdiv_one data()[16] 3.730s passed
seqDef_split_in_three data()[170] 3.908s passed
seqDef_empty data()[171] 3.852s passed
seqDef_one_summand data()[172] 3.900s passed
seqDef_lower_equals_upper data()[173] 3.750s passed
seqDefOfSeq data()[174] 3.792s passed
seqSelfDefinitionEQ2 data()[175] 3.670s passed
indexOfSeqSingleton data()[176] 3.670s passed
indexOfSeqConcatFirst data()[177] 3.720s passed
indexOfSeqConcatSecond data()[178] 3.707s passed
indexOfSeqSub data()[179] 3.781s passed
div_zero data()[17] 3.775s passed
lenOfArray2seq data()[180] 3.735s passed
getAnyOfArray2seq data()[181] 3.735s passed
getOfArray2seq data()[182] 3.783s passed
getAnyOfNPermInv data()[183] 3.729s passed
seqNPermRange data()[184] 3.852s passed
seqPermTrans data()[185] 3.846s passed
seqPermRefl data()[186] 3.754s passed
seqPermSplit data()[187] 3.755s passed
seqNPermRight data()[188] 4.012s passed
seqPermFromSwap data()[189] 3.801s passed
divResZero1 data()[18] 3.811s passed
seqPermTransAlt0 data()[190] 3.684s passed
seqPermTransAlt1 data()[191] 3.805s passed
seqPermTransAlt2 data()[192] 3.658s passed
seqPermTransAlt3 data()[193] 3.792s passed
seqPermForall data()[194] 3.881s passed
seqPermExists data()[195] 3.927s passed
schiffl_lemma_2 data()[196] 25.830s passed
schiffl_thm_1 data()[197] 4.668s passed
eqSameSeq data()[198] 3.908s passed
divResZero2 data()[19] 3.867s passed
eqTermCut data()[1] 4.460s passed
divResOne1 data()[20] 3.738s passed
divResOne2 data()[21] 3.757s passed
div_cancel1 data()[22] 3.757s passed
div_cancel2 data()[23] 3.737s passed
divAddMultDenom data()[24] 3.799s passed
divMinus data()[25] 3.866s passed
divMinusDenom data()[26] 3.849s passed
divLeastDPos data()[27] 3.686s passed
divLeastDNeg data()[28] 3.748s passed
divGreatestDPos data()[29] 3.790s passed
equivAllRight data()[2] 4.188s passed
divGreatestDNeg data()[30] 3.789s passed
divIncreasingPos data()[31] 3.861s passed
divIncreasingNeg data()[32] 3.707s passed
jdiv_zero data()[33] 3.747s passed
jdivPulloutMinusNum data()[34] 3.686s passed
jdivPulloutMinusDenom data()[35] 3.740s passed
jdiv_uniquePosPos data()[36] 3.716s passed
jdiv_uniquePosNeg data()[37] 3.778s passed
jdiv_uniqueNegPos data()[38] 3.852s passed
jdiv_uniqueNegNeg data()[39] 3.763s passed
irrflConcrete1 data()[3] 4.169s passed
jdivMultDenom1 data()[40] 3.832s passed
jdivMultDenom2 data()[41] 3.779s passed
mod_geZero data()[42] 3.678s passed
mod_lessDenom data()[43] 3.712s passed
jmod_NumPos data()[44] 3.812s passed
jmod_NumNeg data()[45] 3.817s passed
jmod_geZero data()[46] 3.881s passed
jmodNumZero data()[47] 3.734s passed
jmod_pulloutminusNum data()[48] 3.719s passed
jmod_pulloutminusDenom data()[49] 3.697s passed
irrflConcrete2 data()[4] 4.065s passed
jmodUnique1 data()[50] 3.920s passed
jmodUnique2 data()[51] 3.895s passed
intDivRem data()[52] 3.871s passed
jmodjmod data()[53] 3.925s passed
jmodDivisible data()[54] 3.879s passed
jmodDivisibleRep data()[55] 3.692s passed
jdivAddMultDenom data()[56] 3.831s passed
jmodAltZero data()[57] 3.743s passed
jmodAddMultDenomZero data()[58] 3.763s passed
polyDiv_zero data()[59] 3.840s passed
cancel_gtPos data()[5] 3.888s passed
polyMod_ltdivDenom data()[60] 3.693s passed
bsum_empty data()[61] 3.723s passed
bsum_induction_upper data()[62] 3.676s passed
bsum_induction_lower data()[63] 3.793s passed
bsum_num_of_bounds data()[64] 3.677s passed
bsum_num_of_bounds2 data()[65] 3.683s passed
bsum_induction_upper2 data()[66] 3.715s passed
bsum_induction_upper_concrete data()[67] 3.711s passed
bsum_induction_upper_concrete_2 data()[68] 3.679s passed
bsum_induction_upper2_concrete data()[69] 3.677s passed
cancel_gtNeg data()[6] 3.805s passed
bsum_induction_lower_concrete data()[70] 3.719s passed
bsum_induction_lower2 data()[71] 3.792s passed
bsum_induction_lower2_concrete data()[72] 3.715s passed
bsum_positive data()[73] 3.835s passed
bsum_upper_bound data()[74] 3.774s passed
bsum_lower_bound data()[75] 3.723s passed
bsum_positive_lower_bound_element data()[76] 3.815s passed
bsum_sub_same_index data()[77] 3.719s passed
bsum_less_same_index data()[78] 3.812s passed
bsum_equal_except_one_index data()[79] 3.846s passed
moduloIntIsInInt data()[7] 3.898s passed
bsum_num_of_is_max data()[80] 3.712s passed
bsum_num_of_is_max2 data()[81] 3.776s passed
bsum_num_of_is_max3 data()[82] 3.817s passed
bsum_num_of_is_max4 data()[83] 3.706s passed
bsum_num_of_lt_max data()[84] 3.884s passed
bsum_num_of_lt_max2 data()[85] 3.786s passed
bsum_num_of_lt_max3 data()[86] 3.751s passed
bsum_num_of_lt_max4 data()[87] 3.771s passed
bsum_num_of_gt0 data()[88] 3.842s passed
bsum_num_of_gt0_alt data()[89] 3.791s passed
moduloLongIsInLong data()[8] 3.816s passed
bsum_add_concrete data()[90] 3.757s passed
bprod_all_positive data()[91] 3.720s passed
bprod_split data()[92] 3.752s passed
powConcrete0 data()[93] 3.802s passed
powConcrete1 data()[94] 3.785s passed
powSplitFactor data()[95] 3.869s passed
powAdd data()[96] 3.736s passed
powMono data()[97] 3.787s passed
powMonoConcrete data()[98] 3.646s passed
powMonoConcreteRight data()[99] 3.662s passed
moduloShortIsInShort data()[9] 3.785s passed

Standard output

369        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
401        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.64ms 
670        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691        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)

1696       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1698       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1700       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1700       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3417       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9795       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.12s 
9901       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9944       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39ns 
9963       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9964       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 706.56ns 
9970       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13215      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
13218      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14409      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.78ms 
14427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14427      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 607.45ns 
14430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17526      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
17526      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18595      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
18610      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.64ms 
18614      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
18614      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.14ns 
18616      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
21704      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
22773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
22781      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
22784      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
22786      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.52ms 
22787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25814      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
25815      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
26840      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
26846      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
26850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
26850      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 526.04ns 
26852      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29733      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
29734      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
30688      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
30735      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.54ms 
30739      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
30739      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 431.24ns 
30741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33561      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
33562      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
34520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
34542      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.62ms 
34545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
34546      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.93ns 
34547      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
37438      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
38435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
38441      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
38443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
38443      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.71ns 
38444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41334      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
41334      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
42254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
42257      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.06ns 
42259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
42259      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.61ns 
42260      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45135      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
45136      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
46039      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
46042      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.46ns 
46044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
46044      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.71ns 
46045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
48893      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
49841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
49844      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 664.43ns 
49846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
49846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.61ns 
49847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52623      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
52623      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
53556      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
53559      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.26ns 
53561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
53561      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.41ns 
53562      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56350      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
56350      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
57271      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
57317      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.89ms 
57319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
57319      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.11ns 
57320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60153      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
60154      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
61077      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
61117      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.6ms 
61119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
61120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.91ns 
61121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63934      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
63935      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
64916      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
65207      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 281.29ms 
65212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
65213      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 531.05ns 
65215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
68022      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
68934      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
68940      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
68941      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
68941      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.91ns 
68942      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71764      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
71765      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
72665      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
72669      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
72672      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
72672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.12ns 
72673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75455      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
75456      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
76399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
76444      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.87ms 
76446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
76446      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.93ns 
76447      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
79269      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
80238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
80255      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms 
80257      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
80258      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.72ns 
80259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83168      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
83169      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
84107      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
84122      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.35ms 
84124      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
84124      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.21ns 
84126      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
86882      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
87835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
87860      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.64ms 
87862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
87863      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.04ns 
87864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90669      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
90669      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
91600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
91617      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.39ms 
91619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
91620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.33ns 
91621      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94424      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
94424      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
95342      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
95374      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.69ms 
95377      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
95377      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.03ns 
95379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98208      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
98209      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
99108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
99111      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
99112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
99113      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.31ns 
99114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
101938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
102865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
102910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.4ms 
102912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
102912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.32ns 
102914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
105741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
106685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
106771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.01ms 
106778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
106778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.81ns 
106780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
109650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
110575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
110624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.05ms 
110627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
110628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.93ns 
110629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
113385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
114302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
114311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.75ms 
114313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
114314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.03ns 
114315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
117071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
118037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
118058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.67ms 
118069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
118070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 470.74ns 
118071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
120952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
121844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
121857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.39ms 
121860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
121860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.53ns 
121861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
124701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
125638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
125646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
125648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
125648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.11ns 
125649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
128533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
129497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
129507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
129510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
129510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.73ns 
129511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
132288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
133206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
133214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.62ms 
133216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
133216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.22ns 
133217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
136015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
136957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
136961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
136963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
136963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.81ns 
136964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
139719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
140637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
140648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms 
140649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
140649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.41ns 
140650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
143411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
144330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
144387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.27ms 
144389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
144389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.81ns 
144390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
147187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
148083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
148103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
148105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
148106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.03ns 
148107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
150914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
151854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
151881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.59ms 
151883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
151884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.71ns 
151885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
154775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
155704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
155733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.27ms 
155735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
155735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.41ns 
155736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
158533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
159472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
159496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.32ms 
159498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
159498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.62ns 
159499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
162361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
163285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
163328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.02ms 
163330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
163330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.41ns 
163331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
166133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
167105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
167108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
167109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
167109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.11ns 
167110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
169867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
170780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
170785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
170786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
170786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.71ns 
170787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
173562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
174488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
174497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.74ms 
174498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
174499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.81ns 
174499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
177331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
178299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
178309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.94ms 
178312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
178313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.13ns 
178314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
181215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
182105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
182126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.75ms 
182128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
182128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.72ns 
182129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
185012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
185997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
186007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.56ms 
186011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
186011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.01ns 
186012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
188809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
189739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
189743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
189745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
189746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.02ns 
189747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
192536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
193458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
193463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
193464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
193464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.81ns 
193465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
196227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
197143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
197156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
197161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
197161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.52ns 
197163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
200039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
200997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
201079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.75ms 
201081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
201081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.41ns 
201083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
203916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
204877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
204974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.54ms 
204976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
204976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.83ns 
204977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
207931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
208841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
208845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
208848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
208848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.63ns 
208849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
211773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
212724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
212770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.96ms 
212772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
212772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.62ns 
212773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
215674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
216608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
216649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.21ms 
216661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
216661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.83ns 
216662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
219434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
220347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
220351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
220352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
220352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.81ns 
220353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
223085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
223995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
224180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 172.54ms 
224183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
224184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.92ns 
224185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
227020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
227912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
227924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.23ms 
227926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
227926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.21ns 
227927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
230780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
231678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
231687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ms 
231688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
231689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.91ns 
231689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
234581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
235509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
235528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.28ms 
235529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
235529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.21ns 
235530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
238281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
239189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
239213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.32ms 
239222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
239222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.61ns 
239223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
242021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
242939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
242943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
242945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
242945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.81ns 
242946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
245701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
246615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
246619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.66ms 
246620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
246621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.31ns 
246621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
249431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
250388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
250413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.67ms 
250414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
250414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.21ns 
250415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
253151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
254072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
254090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.99ms 
254091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
254091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.21ns 
254092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
256867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
257756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
257772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.78ms 
257774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
257774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.91ns 
257775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
260592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
261483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
261487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
261489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
261489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.41ns 
261490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
264272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
265193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
265198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
265199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
265199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.81ns 
265200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
267962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
268871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
268877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
268878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
268878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.21ns 
268879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
271631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
272551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
272554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
272555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
272556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.11ns 
272556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
275335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
276270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
276273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 785.47ns 
276276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
276276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.32ns 
276277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
279141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
280062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
280066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
280068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
280068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.21ns 
280069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
282883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
283779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
283782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
283783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
283783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.81ns 
283784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
286639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
287547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
287616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.45ms 
287618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
287619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.82ns 
287620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
290433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
291344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
291390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.79ms 
291391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
291391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.11ns 
291392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
294161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
295073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
295113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.75ms 
295116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
295117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 592.45ns 
295129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
297956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
298876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
298928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.85ms 
298930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
298930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.71ns 
298931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
301708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
302609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
302647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.12ms 
302648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
302648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.01ns 
302649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
305443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
306400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
306459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.95ms 
306461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
306461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.01ns 
306462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
309331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
310275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
310305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.58ms 
310306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
310306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.91ns 
310307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
313111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
313996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
314017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.38ms 
314019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
314019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.21ns 
314020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
316824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
317762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
317792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.76ms 
317795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
317796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.62ns 
317797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
320682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
321592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
321612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.19ms 
321613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
321613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.11ns 
321614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
324347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
325286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
325317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.98ms 
325319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
325320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.43ns 
325321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
328207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
329173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
329201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.94ms 
329203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
329203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.21ns 
329204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
332035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
332958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
332987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.91ms 
332988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
332988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.41ns 
332989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
335815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
336711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
336738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.3ms 
336740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
336741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.09ms 
336742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
339575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
340484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
340509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.37ms 
340510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
340510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.41ns 
340511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
343397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
344323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
344351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.33ms 
344352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
344352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.11ns 
344353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
347175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
348112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
348142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.39ms 
348143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
348144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.21ns 
348144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
350947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
351891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
351899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.36ms 
351901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
351901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.01ns 
351902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
354683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
355600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
355619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms 
355621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
355621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.41ns 
355622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
358424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
359366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
359371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
359373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
359373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.42ns 
359374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
362268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
363170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
363173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 609.74ns 
363175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
363176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.62ns 
363177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
366057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
366956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
366959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 805.97ns 
366960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
366960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.41ns 
366961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
369877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
370811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
370827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ms 
370832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
370832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.31ns 
370833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
373622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
374556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
374563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
374564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
374564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.51ns 
374565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
377415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
378336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
378350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.21ms 
378352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
378352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.31ns 
378352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
381076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
381993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
381996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
381998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
381998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.91ns 
381999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
384742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
385656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
385658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.35ns 
385659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
385659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.41ns 
385660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
388477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
389358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
389364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
389365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
389365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.01ns 
389366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
392130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
393019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
393021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 621.15ns 
393022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
393022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
393023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
395832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
396787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
396789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 619.55ns 
396791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
396791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.11ns 
396792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
399615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
400531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
400533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.35ns 
400535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
400535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.71ns 
400536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
403301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
404208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
404213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
404215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
404215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.42ns 
404216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
406989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
407912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
407922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.65ms 
407925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
407925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.61ns 
407926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
410689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
411613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
411618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
411619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
411619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.81ns 
411620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
414398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
415315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
415323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
415325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
415325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.31ns 
415326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
418201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
419095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
419099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
419100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
419101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.01ns 
419101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
421915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
422890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
422919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.64ms 
422922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
422922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.22ns 
422924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
425788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
426771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
426775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
426778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
426778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.92ns 
426779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
429530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
430448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
430452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
430453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
430453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
430454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
433198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
434110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
434114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
434116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
434116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.91ns 
434116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
436866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
437776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
437795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.63ms 
437797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
437797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.31ns 
437798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
440572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
441493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
441498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.85ns 
441501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
441501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.82ns 
441502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
444384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
445288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
445332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.52ms 
445334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
445334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.71ns 
445335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
448262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
449148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
449152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
449153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
449153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
449154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
452010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
452973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
452998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.84ms 
453000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
453000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.41ns 
453001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
455844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
456813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
456839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.4ms 
456841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
456841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.61ns 
456842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
459682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
460591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
460618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.96ms 
460620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
460620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.11ns 
460620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
463382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
464305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
464307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 658.85ns 
464308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
464308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
464309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
467133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
468055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
468061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
468062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
468062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
468063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
470992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
471903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
471907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
471908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
471908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.32ns 
471909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
474701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
475624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
475628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.67ns 
475632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
475632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.52ns 
475634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
478532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
479507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
479510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 946.18ns 
479511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
479512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
479512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
482383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
483322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
483326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
483327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
483327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
483328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
486147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
487067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
487070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
487072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
487072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
487072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
489897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
490787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
490799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.51ms 
490800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
490801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.31ns 
490801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
493564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
494494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
494511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.28ms 
494520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
494520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.72ns 
494522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
497336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
498300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
498312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.33ms 
498314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
498314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.51ns 
498314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
501217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
502190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
502213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.75ms 
502215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
502215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.21ns 
502216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
505024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
506000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
506006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
506008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
506008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.61ns 
506008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
508962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
509895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
509902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
509903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
509903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.91ns 
509904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
512724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
513713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
513716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 741.07ns 
513717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
513717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.51ns 
513718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
516508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
517456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
517460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
517462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
517462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.41ns 
517462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
520248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
521187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
521189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 935.98ns 
521190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
521190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.01ns 
521191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
524044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
524978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
524992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.79ms 
524994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
524994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.42ns 
524995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
527807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
528741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
528745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
528747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
528747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.61ns 
528747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
531580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
532487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
532495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
532496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
532496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.41ns 
532497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
535257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
536189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
536191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 816.88ns 
536192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
536192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.31ns 
536193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
539019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
539978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
539980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 778.87ns 
539981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
539982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.41ns 
539982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
542864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
543773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
543777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
543778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
543778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.31ns 
543779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
546530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
547489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
547493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
547494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
547494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.91ns 
547495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
550381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
551307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
551311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
551312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
551312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
551313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
554107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
555034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
555037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
555039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
555039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.31ns 
555040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
557856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
558805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
558811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
558813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
558813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.21ns 
558813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
561612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
562508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
562512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
562513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
562513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.41ns 
562514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
565286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
566228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
566241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms 
566243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
566243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.12ns 
566244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
569021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
569960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
569963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 824.77ns 
569964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
569964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.11ns 
569965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
572813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
573736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
573744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
573745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
573745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.41ns 
573746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
576503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
577438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
577441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
577442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
577442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
577443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
580238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
581181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
581184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 929.98ns 
581185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
581185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.61ns 
581186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
583966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
584893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
584898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
584900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
584900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
584901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
587706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
588605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
588608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
588609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
588610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.21ns 
588610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
591391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
592342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
592345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
592347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
592347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.11ns 
592348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
595113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
596012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
596017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
596018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
596018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.21ns 
596019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
598833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
599774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
599780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.96ms 
599781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
599782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.41ns 
599783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
602628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
603528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
603544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
603545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
603546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.61ns 
603546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
606368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
607329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
607351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.97ms 
607353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
607353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.82ns 
607354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
610261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
611236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
611250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.14ms 
611252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
611252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.31ns 
611253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
614077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
614991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
615003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
615005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
615005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.71ns 
615005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
617793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
618713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
618743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.76ms 
618744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
618744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.31ns 
618745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
621483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
622407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
622436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.26ms 
622437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
622437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.61ns 
622438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
625171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
626089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
626116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.75ms 
626118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
626118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.31ns 
626118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
628880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
629812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
629829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
629830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
629830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.11ns 
629831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
632599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
633520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
633555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.66ms 
633556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
633556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.01ns 
633557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
636434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
637401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
637460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.44ms 
637461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
637461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.81ns 
637462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
640275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
641181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
641226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.89ms 
641228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
641228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.81ns 
641228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
644061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
644992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
645040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.46ms 
645041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
645041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.61ns 
645042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
647825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
648746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
648796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.48ms 
648797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
648797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.51ns 
648798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
651570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
652551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
652703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 144.16ms 
652705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
652705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.31ns 
652705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
655569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
656546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
656555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.92ms 
656557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
656557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.51ns 
656558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
659501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
660447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
660455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.67ms 
660457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
660457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.81ns 
660458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
663276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
664200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
664206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
664207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
664207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.31ns 
664208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
667036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
667975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
667997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.82ms 
667998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
667998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.31ns 
667999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
670735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
671655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
671668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.28ms 
671669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
671669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.61ns 
671670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
674414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
675333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
675337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
675338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
675338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.31ns 
675339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
678107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
679038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
679057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.76ms 
679058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
679058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.81ns 
679059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
681841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
682746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
682765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.88ms 
682766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
682766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.61ns 
682767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
685565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
686519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
686545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.54ms 
686548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
686548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.12ns 
686549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
689347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
690277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
690280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
690282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
690282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.51ns 
690282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
693049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
694011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
694015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
694016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
694016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.91ns 
694017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
696859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
697791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
697798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
697800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
697800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.81ns 
697800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
700617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
701520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
701527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
701528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
701528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.01ns 
701529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
704326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
705293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
705379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.17ms 
705381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
705382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 714.46ns 
705383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
708256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
709189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
709226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.55ms 
709227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
709227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.41ns 
709228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
712017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
712954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
712980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.88ms 
712981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
712981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.61ns 
712982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
715800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
716732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
716734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 319.83ns 
716735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
716735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
716737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
719503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
720484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
720746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 249.2ms 
720749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
720749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.82ns 
720750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
723560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
724489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
724547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.9ms 
724549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
724549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.61ns 
724550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
727308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
728229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
728231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 369.53ns 
728233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
728233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
728233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
731059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
732034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
732036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 401.44ns 
732037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
732038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.01ns 
732038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
734772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
735693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
735695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 403.74ns 
735696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
735696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
735697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
738552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
739484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
739487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.85ns 
739488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
739488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.41ns 
739489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
742289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
743251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
743367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.31ms 
743369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
743370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.14ns 
743372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
746242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
747239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
747295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.42ms 
747296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
747296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
747298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
750212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
751148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
751149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
751179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
751232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
751260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
751268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
751278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
751281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
751282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
751285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
751290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
751292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
751297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
751299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
751523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
751524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
751525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
751526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
751527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
751650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
751651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
751653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
751654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
751656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
751657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
751838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
751840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
751841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
751842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
751843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
751845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
751979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
751981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
751982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
751983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
751984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
751985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
751993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
751994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
751995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
751997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
751998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
751999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
752007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
752008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
752008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
752010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
752010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
752011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
752166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
752167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
752169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
752316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
752318     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)'' 
752321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
752322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
752323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
752324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
752325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
752326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
752332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
752334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
752336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
752337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
752338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
752457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
752462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
752464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
752465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
752466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
752467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
752468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
752596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
752598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
752599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
752601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
752602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
752603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
752605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
752606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
752702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
752704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
752831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
752838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
752846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
752847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
752849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
752850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
752851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
752852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
752852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
752854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
752865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
752873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
752996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
752997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
752998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
753000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
753000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
753001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
753002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
753003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
753060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
753066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
753170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
753172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
753174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
753176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
753176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
753177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
753318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
753322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
753324     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)'' 
753326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
753327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
753328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
753329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
753330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
753339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
753341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
753342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
753343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
753448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
753455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
753456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
753457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
753458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
753459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
753575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
753577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
753578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
753579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
753580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
753581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
753581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
753583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
753674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
753676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
753830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
753830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
753831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
753835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
753839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
753843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
754018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
754020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
754021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
754022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
754033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
754127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
758063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
758064     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)'' 
758070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
758071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
758072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
758073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
758074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
758083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
758084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
758085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
758086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
758087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
758196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
758202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
758204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
758205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
758206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
758206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
758207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
758316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
758318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
758319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
758320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
758321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
758322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
758322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
758324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
758411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
758413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
758498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
758503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
758507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
758509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
758510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
758511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
758522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
758659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
758661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
758662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
758663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
758747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
758758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
758759     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)'' 
758761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
758762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
758763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
758764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
758765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
758777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
758779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
758780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
758781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
758782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
758885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
758887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
758888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
758889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
758890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
758997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
759002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
759003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
759004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
759005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
759006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
759007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
759123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
759125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
759126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
759128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
759129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
759130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
759130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
759132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
759133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
759134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
759135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
759136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
759136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
759137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
759138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
759240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
759242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
759249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
759340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
759434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
759436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
759437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
759438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
759439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
759440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
759441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
759441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
759442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
759543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
759550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
759659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
759660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
759661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
759662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
759663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
759663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
759664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
759665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
759670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
759671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
759767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
759773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
759779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
759898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
759899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
759900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
759901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
759902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
759902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
759903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
759903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
759967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
759968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
759969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
759969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
759970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
759976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
759981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
760116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
760218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
760219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
760220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
760221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
760413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
760514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
760515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
764092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
764099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
764100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
764101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
764102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
764237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
764239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
764240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
764241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
764242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
764367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
767948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
771683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
771689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
771690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
771691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
771691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
771823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
771825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
771826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
771827     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)' ...' 
771829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
773126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
773126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.91ns 
773127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
776030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
776986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
776988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
776988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
776998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
777011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
777014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
777016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
777016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
777021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
777023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
777026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
777029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
777030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
777040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
777042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
777043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
777100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
777101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
777102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
777103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
777103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
777179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
777180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
777182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
777183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
777183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
777188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
777188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
777189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
777190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
777191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
777192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
777286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
777287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
777287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
777289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
777290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
777291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
777386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
777387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
777388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
777389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
777390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
777391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
777391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
777392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
777393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
777394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
777394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
777395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
777395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
777396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
777397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
777397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
777398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
777399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
777400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
777403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
777447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
777448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
777517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
777519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
777521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
777522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
777523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
777524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
777581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
777584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
777585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
777587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
777588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
777589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
777590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
777646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
777649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
777653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
777723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
777794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
777794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.42ns 
777795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
780673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
781660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
781700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.47ms